DEFINITION simpl_lt_plus_r()
TYPE =
       ∀p:nat.∀n:nat.∀m:nat.(lt (plus n p) (plus m p))→(lt n m)
BODY =
        assume p: nat
        assume n: nat
        assume m: nat
        suppose H: lt (plus n p) (plus m p)
          (H0) 
             by (plus_sym . .)
             we proved eq nat (plus n p) (plus p n)
             we proceed by induction on the previous result to prove lt (plus p n) (plus m p)
                case refl_equal : ⇒
                   the thesis becomes the hypothesis H
lt (plus p n) (plus m p)
          end of H0
          (H1) 
             by (plus_sym . .)
             we proved eq nat (plus m p) (plus p m)
             we proceed by induction on the previous result to prove lt (plus p n) (plus p m)
                case refl_equal : ⇒
                   the thesis becomes the hypothesis H0
lt (plus p n) (plus p m)
          end of H1
          consider H1
          we proved lt (plus p n) (plus p m)
          by (simpl_lt_plus_l . . . previous)
          we proved lt n m
       we proved ∀p:nat.∀n:nat.∀m:nat.(lt (plus n p) (plus m p))→(lt n m)