DEFINITION S_pred()
TYPE =
       ∀n:nat.∀m:nat.(lt m n)→(eq nat n (S (pred n)))
BODY =
        assume n: nat
        assume m: nat
        suppose H: lt m n
          consider H
          we proved lt m n
          that is equivalent to le (S m) n
          we proceed by induction on the previous result to prove eq nat n (S (pred n))
             case le_n : ⇒
                the thesis becomes eq nat (S m) (S (pred (S m)))
                   by (refl_equal . .)
                   we proved eq nat (S (pred (S m))) (S (pred (S m)))
eq nat (S m) (S (pred (S m)))
             case le_S : m0:nat :le (S m) m0 ⇒
                the thesis becomes eq nat (S m0) (S (pred (S m0)))
                () by induction hypothesis we know eq nat m0 (S (pred m0))
                   by (refl_equal . .)
                   we proved eq nat (S (pred (S m0))) (S (pred (S m0)))
eq nat (S m0) (S (pred (S m0)))
          we proved eq nat n (S (pred n))
       we proved ∀n:nat.∀m:nat.(lt m n)→(eq nat n (S (pred n)))