DEFINITION le_n_pred()
TYPE =
       ∀n:nat.∀m:nat.(le n m)→(le (pred n) (pred m))
BODY =
        assume n: nat
        assume m: nat
        suppose H: le n m
          we proceed by induction on H to prove le (pred n) (pred m)
             case le_n : ⇒
                the thesis becomes le (pred n) (pred n)
                   by (le_n .)
le (pred n) (pred n)
             case le_S : m0:nat :le n m0 ⇒
                the thesis becomes le (pred n) (pred (S m0))
                (H1) by induction hypothesis we know le (pred n) (pred m0)
                   by (le_pred_n .)
                   we proved le (pred m0) m0
                   by (le_trans . . . H1 previous)
                   we proved le (pred n) m0
le (pred n) (pred (S m0))
          we proved le (pred n) (pred m)
       we proved ∀n:nat.∀m:nat.(le n m)→(le (pred n) (pred m))