DEFINITION lt_eq_e()
TYPE =
       ∀x:nat
         .∀y:nat
           .∀P:Prop
             .((lt x y)→P)→((eq nat x y)→P)→(le x y)→P
BODY =
Show proof