DEFINITION le_lt_trans()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(le n m)→(lt m p)→(lt n p)
BODY =
        assume n: nat
        assume m: nat
        assume p: nat
        suppose H: le n m
        suppose H0: lt m p
          consider H0
          we proved lt m p
          that is equivalent to le (S m) p
          we proceed by induction on the previous result to prove lt n p
             case le_n : ⇒
                the thesis becomes lt n (S m)
                   by (le_n_S . . H)
                   we proved le (S n) (S m)
lt n (S m)
             case le_S : m0:nat :le (S 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.(le n m)→(lt m p)→(lt n p)