DEFINITION le_or_lt()
TYPE =
       ∀n:nat.∀m:nat.(or (le n m) (lt m n))
BODY =
        assume n: nat
        assume m: nat
          (h1) 
             assume n0: nat
                by (le_O_n .)
                we proved le O n0
                by (or_introl . . previous)
                we proved or (le O n0) (lt n0 O)
∀n0:nat.(or (le O n0) (lt n0 O))
          end of h1
          (h2) 
             assume n0: nat
                by (lt_O_Sn .)
                we proved lt O (S n0)
                by (lt_le_S . . previous)
                we proved le (S O) (S n0)
                that is equivalent to lt O (S n0)
                by (or_intror . . previous)
                we proved or (le (S n0) O) (lt O (S n0))
∀n0:nat.(or (le (S n0) O) (lt O (S n0)))
          end of h2
          (h3) 
              assume n0: nat
              assume m0: nat
              suppose H: or (le n0 m0) (lt m0 n0)
                we proceed by induction on H to prove or (le (S n0) (S m0)) (lt (S m0) (S n0))
                   case or_introl : H0:le n0 m0 ⇒
                      the thesis becomes or (le (S n0) (S m0)) (lt (S m0) (S n0))
                         by (le_n_S . . H0)
                         we proved le (S n0) (S m0)
                         by (or_introl . . previous)
or (le (S n0) (S m0)) (lt (S m0) (S n0))
                   case or_intror : H0:lt m0 n0 ⇒
                      the thesis becomes or (le (S n0) (S m0)) (lt (S m0) (S n0))
                         consider H0
                         we proved lt m0 n0
                         that is equivalent to le (S m0) n0
                         by (le_n_S . . previous)
                         we proved le (S (S m0)) (S n0)
                         that is equivalent to lt (S m0) (S n0)
                         by (or_intror . . previous)
or (le (S n0) (S m0)) (lt (S m0) (S n0))
                we proved or (le (S n0) (S m0)) (lt (S m0) (S n0))

                ∀n0:nat
                  .∀m0:nat.(or (le n0 m0) (lt m0 n0))→(or (le (S n0) (S m0)) (lt (S m0) (S n0)))
          end of h3
          by (nat_double_ind . h1 h2 h3 . .)
          we proved or (le n m) (lt m n)
       we proved ∀n:nat.∀m:nat.(or (le n m) (lt m n))