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