DEFINITION O_minus()
TYPE =
       ∀x:nat.∀y:nat.(le x y)→(eq nat (minus x y) O)
BODY =
       assume x: nat
          we proceed by induction on x to prove ∀y:nat.(le x y)→(eq nat (minus x y) O)
             case O : ⇒
                the thesis becomes ∀y:nat.(le O y)→(eq nat (minus O y) O)
                    assume y: nat
                    suppose : le O y
                      by (refl_equal . .)
                      we proved eq nat O O
                      that is equivalent to eq nat (minus O y) O
∀y:nat.(le O y)→(eq nat (minus O y) O)
             case S : x0:nat ⇒
                the thesis becomes 
                ∀y:nat
                  .le (S x0) y
                    →eq nat <λn1:nat.nat> CASE y OF O⇒S x0 | S l⇒minus x0 l O
                (H) by induction hypothesis we know ∀y:nat.(le x0 y)→(eq nat (minus x0 y) O)
                   assume y: nat
                      we proceed by induction on y to prove 
                         le (S x0) y
                           →eq nat <λn1:nat.nat> CASE y OF O⇒S x0 | S l⇒minus x0 l O
                         case O : ⇒
                            the thesis becomes 
                            le (S x0) O
                              →eq nat <λn1:nat.nat> CASE O OF O⇒S x0 | S l⇒minus x0 l O
                               suppose H0: le (S x0) O
                                  by (le_gen_S . . H0)
                                  we proved ex2 nat λn:nat.eq nat O (S n) λn:nat.le x0 n
                                  we proceed by induction on the previous result to prove eq nat (S x0) O
                                     case ex_intro2 : x1:nat H1:eq nat O (S x1) :le x0 x1 ⇒
                                        the thesis becomes eq nat (S x0) O
                                           (H3) 
                                              we proceed by induction on H1 to prove <λ:nat.Prop> CASE S x1 OF O⇒True | S ⇒False
                                                 case refl_equal : ⇒
                                                    the thesis becomes <λ:nat.Prop> CASE O OF O⇒True | S ⇒False
                                                       consider I
                                                       we proved True
<λ:nat.Prop> CASE O OF O⇒True | S ⇒False
<λ:nat.Prop> CASE S x1 OF O⇒True | S ⇒False
                                           end of H3
                                           consider H3
                                           we proved <λ:nat.Prop> CASE S x1 OF O⇒True | S ⇒False
                                           that is equivalent to False
                                           we proceed by induction on the previous result to prove eq nat (S x0) O
eq nat (S x0) O
                                  we proved eq nat (S x0) O
                                  that is equivalent to eq nat <λn1:nat.nat> CASE O OF O⇒S x0 | S l⇒minus x0 l O

                                  le (S x0) O
                                    →eq nat <λn1:nat.nat> CASE O OF O⇒S x0 | S l⇒minus x0 l O
                         case S : n:nat ⇒
                            the thesis becomes ∀H1:(le (S x0) (S n)).(eq nat (minus x0 n) O)
                            () by induction hypothesis we know 
                               le (S x0) n
                                 →eq nat <λn1:nat.nat> CASE n OF O⇒S x0 | S l⇒minus x0 l O
                               suppose H1: le (S x0) (S n)
                                  by (le_S_n . . H1)
                                  we proved le x0 n
                                  by (H . previous)
                                  we proved eq nat (minus x0 n) O
                                  that is equivalent to eq nat <λn1:nat.nat> CASE S n OF O⇒S x0 | S l⇒minus x0 l O
∀H1:(le (S x0) (S n)).(eq nat (minus x0 n) O)
                      we proved 
                         le (S x0) y
                           →eq nat <λn1:nat.nat> CASE y OF O⇒S x0 | S l⇒minus x0 l O
                      that is equivalent to (le (S x0) y)→(eq nat (minus (S x0) y) O)

                      ∀y:nat
                        .le (S x0) y
                          →eq nat <λn1:nat.nat> CASE y OF O⇒S x0 | S l⇒minus x0 l O
          we proved ∀y:nat.(le x y)→(eq nat (minus x y) O)
       we proved ∀x:nat.∀y:nat.(le x y)→(eq nat (minus x y) O)