DEFINITION le_pred_n()
TYPE =
       ∀n:nat.(le (pred n) n)
BODY =
       assume n: nat
          we proceed by induction on n to prove le (pred n) n
             case O : ⇒
                the thesis becomes le (pred O) O
                   by (le_n .)
                   we proved le O O
le (pred O) O
             case S : n0:nat ⇒
                the thesis becomes le (pred (S n0)) (S n0)
                () by induction hypothesis we know le (pred n0) n0
                   by (le_n .)
                   we proved le n0 n0
                   that is equivalent to le (pred (S n0)) n0
                   by (le_S . . previous)
le (pred (S n0)) (S n0)
          we proved le (pred n) n
       we proved ∀n:nat.(le (pred n) n)