DEFINITION le_plus_l()
TYPE =
       ∀n:nat.∀m:nat.(le n (plus n m))
BODY =
       assume n: nat
          we proceed by induction on n to prove ∀m:nat.(le n (plus n m))
             case O : ⇒
                the thesis becomes ∀m:nat.(le O (plus O m))
                   assume m: nat
                      by (le_O_n .)
                      we proved le O m
                      that is equivalent to le O (plus O m)
∀m:nat.(le O (plus O m))
             case S : n0:nat ⇒
                the thesis becomes ∀m:nat.(le (S n0) (S (plus n0 m)))
                (IHn) by induction hypothesis we know ∀m:nat.(le n0 (plus n0 m))
                   assume m: nat
                      by (IHn .)
                      we proved le n0 (plus n0 m)
                      by (le_n_S . . previous)
                      we proved le (S n0) (S (plus n0 m))
                      that is equivalent to le (S n0) (plus (S n0) m)
∀m:nat.(le (S n0) (S (plus n0 m)))
          we proved ∀m:nat.(le n (plus n m))
       we proved ∀n:nat.∀m:nat.(le n (plus n m))