DEFINITION le_lt_or_eq()
TYPE =
       ∀n:nat.∀m:nat.(le n m)→(or (lt n m) (eq nat n m))
BODY =
        assume n: nat
        assume m: nat
        suppose H: le n m
          we proceed by induction on H to prove or (lt n m) (eq nat n m)
             case le_n : ⇒
                the thesis becomes or (lt n n) (eq nat n n)
                   by (refl_equal . .)
                   we proved eq nat n n
                   by (or_intror . . previous)
or (lt n n) (eq nat n n)
             case le_S : m0:nat H0:le n m0 ⇒
                the thesis becomes or (lt n (S m0)) (eq nat n (S m0))
                () by induction hypothesis we know or (lt n m0) (eq nat n m0)
                   by (le_n_S . . H0)
                   we proved le (S n) (S m0)
                   that is equivalent to lt n (S m0)
                   by (or_introl . . previous)
or (lt n (S m0)) (eq nat n (S m0))
          we proved or (lt n m) (eq nat n m)
       we proved ∀n:nat.∀m:nat.(le n m)→(or (lt n m) (eq nat n m))