DEFINITION lt_le_trans()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(lt n m)→(le m p)→(lt n p)
BODY =
Show proof