DEFINITION le_ind()
TYPE =
       ∀n:nat
         .∀P:nat→Prop
           .P n
             →(∀n1:nat.(le n n1)→(P n1)→(P (S n1)))→∀n1:nat.(le n n1)→(P n1)
BODY =
Show proof