DEFINITION minus_le()
TYPE =
       ∀x:nat.∀y:nat.(le (minus x y) x)
BODY =
       assume x: nat
          we proceed by induction on x to prove ∀y:nat.(le (minus x y) x)
             case O : ⇒
                the thesis becomes nat→(le (minus O __1) O)
                   assume : nat
                      by (le_n .)
                      we proved le O O
                      that is equivalent to le (minus O __1) O
nat→(le (minus O __1) O)
             case S : n:nat ⇒
                the thesis becomes ∀y:nat.(le (minus (S n) y) (S n))
                (H) by induction hypothesis we know ∀y:nat.(le (minus n y) n)
                   assume y: nat
                      we proceed by induction on y to prove le (minus (S n) y) (S n)
                         case O : ⇒
                            the thesis becomes le (minus (S n) O) (S n)
                               by (le_n .)
                               we proved le (S n) (S n)
le (minus (S n) O) (S n)
                         case S : n0:nat ⇒
                            the thesis becomes le (minus (S n) (S n0)) (S n)
                            () by induction hypothesis we know le <λn1:nat.nat> CASE n0 OF O⇒S n | S l⇒minus n l (S n)
                               by (H .)
                               we proved le (minus n n0) n
                               by (le_S . . previous)
                               we proved le (minus n n0) (S n)
le (minus (S n) (S n0)) (S n)
                      we proved le (minus (S n) y) (S n)
∀y:nat.(le (minus (S n) y) (S n))
          we proved ∀y:nat.(le (minus x y) x)
       we proved ∀x:nat.∀y:nat.(le (minus x y) x)