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