DEFINITION le_lt_or_eq()
TYPE =
       ∀n:nat.∀m:nat.(le n m)→(or (lt n m) (eq nat n m))
BODY =
Show proof