DEFINITION le_elim_rel()
TYPE =
       ∀P:nat→nat→Prop
         .∀p:nat.(P O p)
           →(∀p:nat.∀q:nat.(le p q)→(P p q)→(P (S p) (S q))
                →∀n:nat.∀m:nat.(le n m)→(P n m))
BODY =
        assume P: nat→nat→Prop
        suppose H: ∀p:nat.(P O p)
        suppose H0: ∀p:nat.∀q:nat.(le p q)→(P p q)→(P (S p) (S q))
        assume n: nat
          we proceed by induction on n to prove ∀m:nat.(le n m)→(P n m)
             case O : ⇒
                the thesis becomes ∀m:nat.(le O m)→(P O m)
                    assume m: nat
                    suppose : le O m
                      by (H .)
                      we proved P O m
∀m:nat.(le O m)→(P O m)
             case S : n0:nat ⇒
                the thesis becomes ∀m:nat.∀Le:(le (S n0) m).(P (S n0) m)
                (IHn) by induction hypothesis we know ∀m:nat.(le n0 m)→(P n0 m)
                    assume m: nat
                    suppose Le: le (S n0) m
                      we proceed by induction on Le to prove P (S n0) m
                         case le_n : ⇒
                            the thesis becomes P (S n0) (S n0)
                               (h1) by (le_n .) we proved le n0 n0
                               (h2) 
                                  by (le_n .)
                                  we proved le n0 n0
                                  by (IHn . previous)
P n0 n0
                               end of h2
                               by (H0 . . h1 h2)
P (S n0) (S n0)
                         case le_S : m0:nat H1:le (S n0) m0 ⇒
                            the thesis becomes P (S n0) (S m0)
                            () by induction hypothesis we know P (S n0) m0
                               (h1) 
                                  by (le_trans_S . . H1)
le n0 m0
                               end of h1
                               (h2) 
                                  by (le_trans_S . . H1)
                                  we proved le n0 m0
                                  by (IHn . previous)
P n0 m0
                               end of h2
                               by (H0 . . h1 h2)
P (S n0) (S m0)
                      we proved P (S n0) m
∀m:nat.∀Le:(le (S n0) m).(P (S n0) m)
          we proved ∀m:nat.(le n m)→(P n m)
       we proved 
          ∀P:nat→nat→Prop
            .∀p:nat.(P O p)
              →(∀p:nat.∀q:nat.(le p q)→(P p q)→(P (S p) (S q))
                   →∀n:nat.∀m:nat.(le n m)→(P n m))