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 =
        assume x: nat
        assume y: nat
        assume P: Prop
        suppose H: (lt x y)→P
        suppose H0: (eq nat x y)→P
        suppose H1: (lt y x)→P
          suppose H2: le y x
             suppose H3: eq nat y x
                by (sym_eq . . . H3)
                we proved eq nat x y
                by (H0 previous)
                we proved P
             we proved (eq nat y x)→P
             by (lt_eq_e . . . H1 previous H2)
             we proved P
          we proved (le y x)→P
          by (lt_le_e . . . H previous)
          we proved P
       we proved 
          ∀x:nat
            .∀y:nat
              .∀P:Prop
                .(lt x y)→P
                  →((eq nat x y)→P)→((lt y x)→P)→P