DEFINITION lt_le_e()
TYPE =
       ∀n:nat.∀d:nat.∀P:Prop.((lt n d)→P)→((le d n)→P)→P
BODY =
        assume n: nat
        assume d: nat
        assume P: Prop
        suppose H: (lt n d)→P
        suppose H0: (le d n)→P
          (H1) 
             by (le_or_lt . .)
or (le d n) (lt n d)
          end of H1
          we proceed by induction on H1 to prove P
             case or_introl ⇒
                the thesis becomes the hypothesis H0
             case or_intror ⇒
                the thesis becomes the hypothesis H
          we proved P
       we proved ∀n:nat.∀d:nat.∀P:Prop.((lt n d)→P)→((le d n)→P)→P