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 =
        assume x: nat
        assume y: nat
        assume P: Prop
        suppose H: (lt x y)→P
        suppose H0: (eq nat x y)→P
        suppose H1: le x y
          by (le_lt_or_eq . . H1)
          we proved or (lt x y) (eq nat x y)
          we proceed by induction on the previous result to prove P
             case or_introl ⇒
                the thesis becomes the hypothesis H
             case or_intror ⇒
                the thesis becomes the hypothesis H0
          we proved P
       we proved 
          ∀x:nat
            .∀y:nat
              .∀P:Prop
                .((lt x y)→P)→((eq nat x y)→P)→(le x y)→P