DEFINITION simpl_le_plus_l()
TYPE =
       ∀p:nat.∀n:nat.∀m:nat.(le (plus p n) (plus p m))→(le n m)
BODY =
       assume p: nat
          we proceed by induction on p to prove ∀n0:nat.∀m:nat.(le (plus p n0) (plus p m))→(le n0 m)
             case O : ⇒
                the thesis becomes ∀n:nat.∀m:nat.(le (plus O n) (plus O m))→(le n m)
                    assume n: nat
                    assume m: nat
                      we must prove (le (plus O n) (plus O m))→(le n m)
                      or equivalently (le n m)→(le n m)
                      suppose H: le n m
                         consider H
                      we proved (le n m)→(le n m)
                      that is equivalent to (le (plus O n) (plus O m))→(le n m)
∀n:nat.∀m:nat.(le (plus O n) (plus O m))→(le n m)
             case S : p0:nat ⇒
                the thesis becomes ∀n:nat.∀m:nat.(le (plus (S p0) n) (plus (S p0) m))→(le n m)
                (IHp) by induction hypothesis we know ∀n:nat.∀m:nat.(le (plus p0 n) (plus p0 m))→(le n m)
                    assume n: nat
                    assume m: nat
                      we must prove (le (plus (S p0) n) (plus (S p0) m))→(le n m)
                      or equivalently (le (S (plus p0 n)) (S (plus p0 m)))→(le n m)
                      suppose H: le (S (plus p0 n)) (S (plus p0 m))
                         by (le_S_n . . H)
                         we proved le (plus p0 n) (plus p0 m)
                         by (IHp . . previous)
                         we proved le n m
                      we proved (le (S (plus p0 n)) (S (plus p0 m)))→(le n m)
                      that is equivalent to (le (plus (S p0) n) (plus (S p0) m))→(le n m)
∀n:nat.∀m:nat.(le (plus (S p0) n) (plus (S p0) m))→(le n m)
          we proved ∀n0:nat.∀m:nat.(le (plus p n0) (plus p m))→(le n0 m)
       we proved ∀p:nat.∀n0:nat.∀m:nat.(le (plus p n0) (plus p m))→(le n0 m)