------------------------------------------------------------------------------
[]
------------------------------------------------------------------------------
                                      (   n : Nat    !
data (---------!  where zero : Nat ;  !--------------!
     ! Nat : * )                      ! succ n : Nat )
------------------------------------------------------------------------------
[]
------------------------------------------------------------------------------
     (   m, n : Nat   !                    
let  !----------------!                    
     ! plus m n : Nat )                    
                                           
     plus m n <= rec m                     
     { plus m n <= case m                  
       { plus zero n => n                  
         plus (succ m) n => succ (plus m n)
       }                                   
     }                                     
------------------------------------------------------------------------------
[]
------------------------------------------------------------------------------
data (---------!  where lt, eq, gt : Ord
     ! Ord : * )                        
------------------------------------------------------------------------------
[]
------------------------------------------------------------------------------
     (    m, n : Nat    !                          
let  !------------------!                          
     ! ordNat m n : Ord )                          
                                                   
     ordNat m n <= rec m                           
     { ordNat m n <= rec n                         
       { ordNat m n <= case m                      
         { ordNat zero n <= case n                 
           { ordNat zero zero => eq                
             ordNat zero (succ n) => lt            
           }                                       
           ordNat (succ m) n <= case n             
           { ordNat (succ m) zero => gt            
             ordNat (succ m) (succ n) => ordNat m n
           }                                       
         }                                         
       }                                           
     }                                             
------------------------------------------------------------------------------
[]
------------------------------------------------------------------------------
     ( m, n : Nat !        (     m : Nat     !    (   p : Lt m n    !
data !------------!  where !-----------------! ;  !-----------------!
     ! Lt m n : * )        ! lt0 m :         !    ! ltS p :         !
                           !   Lt m (succ m) )    !   Lt m (succ n) )
------------------------------------------------------------------------------
[]
------------------------------------------------------------------------------
     (          n : Nat           !     
let  !----------------------------!     
     ! ordLt n : Lt zero (succ n) )     
                                        
     ordLt n <= rec n                   
     { ordLt n <= case n                
       { ordLt zero => lt0 ?            
         ordLt (succ n) => ltS (ordLt n)
       }                                
     }                                  
------------------------------------------------------------------------------
     ( m, n : Nat !        (     n : Nat     !    (   p : Gt m n    !
data !------------!  where !-----------------! ;  !-----------------!
     ! Gt m n : * )        ! gt0 n :         !    ! gtS p :         !
                           !   Gt (succ n) n )    !   Gt (succ m) n )
------------------------------------------------------------------------------
     (          m : Nat           !     
let  !----------------------------!     
     ! ordGt m : Gt (succ m) zero )     
                                        
     ordGt m <= rec m                   
     { ordGt m <= case m                
       { ordGt zero => gt0 ?            
         ordGt (succ m) => gtS (ordGt m)
       }                                
     }                                  
------------------------------------------------------------------------------
     ( m, n : Nat !        ( p : Lt m n !    (  k : Nat   !    ( p : Gt m n !
data !------------!  where !------------! ;  !------------! ;  !------------!
     ! OrdNat m n !        ! OrdLt p :  !    ! OrdEq k :  !    ! OrdGt p :  !
     !  : *       )        !   OrdNat m !    !   OrdNat k !    !   OrdNat m !
                           !   % n      )    !   % k      )    !   % n      )
------------------------------------------------------------------------------
let  (-------------------------!                        
     ! ordnat m n : OrdNat m n )                        
                                                        
     ordnat m n <= rec m                                
     { ordnat m n <= rec n                              
       { ordnat m n <= case m                           
         { ordnat zero n <= case n                      
           { ordnat zero zero => OrdEq zero             
             ordnat zero (succ n) => OrdLt (ordLt n)    
           }                                            
           ordnat (succ m) n <= case n                  
           { ordnat (succ m) zero => OrdGt (ordGt m)    
             ordnat (succ m) (succ n) <= view ordnat m n
             { ordnat (succ m) (succ n) []              
               ordnat (succ k) (succ k) []              
               ordnat (succ m) (succ n) []              
             }                                          
           }                                            
         }                                              
       }                                                
     }                                                  
------------------------------------------------------------------------------