DEFINITION lt_le_trans()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(lt n m)→(le m p)→(lt n p)
BODY =
        assume n: nat
        assume m: nat
        assume p: nat
        suppose H: lt n m
        suppose H0: le m p
          we proceed by induction on H0 to prove lt n p
             case le_n : ⇒
                the thesis becomes the hypothesis H
             case le_S : m0:nat :le m m0 ⇒
                the thesis becomes lt n (S m0)
                (IHle) by induction hypothesis we know lt n m0
                   consider IHle
                   we proved lt n m0
                   that is equivalent to le (S n) m0
                   by (le_S . . previous)
                   we proved le (S n) (S m0)
lt n (S m0)
          we proved lt n p
       we proved ∀n:nat.∀m:nat.∀p:nat.(lt n m)→(le m p)→(lt n p)