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