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