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 =
        assume n: nat
        assume P: nat→Prop
        suppose H: P n
        suppose H1: ∀n1:nat.(le n n1)→(P n1)→(P (S n1))
          (aux) by well-founded reasoning we prove ∀n1:nat.(le n n1)→(P n1)
           assume n1: nat
           suppose H2: le n n1
             by cases on H2 we prove P n1
                case le_n ⇒
                   the thesis becomes the hypothesis H
                case le_S n2:nat H3:le n n2 ⇒
                   the thesis becomes P (S n2)
                   by (aux . H3)
                   we proved P n2
                   by (H1 . H3 previous)
P (S n2)
             we proved P n1
∀n1:nat.(le n n1)→(P n1)
          done
          consider aux
          we proved ∀n1:nat.(le n n1)→(P n1)
       we proved 
          ∀n:nat
            .∀P:nat→Prop
              .P n
                →(∀n1:nat.(le n n1)→(P n1)→(P (S n1)))→∀n1:nat.(le n n1)→(P n1)