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 =
Show proof