DEFINITION plus_n_Sm()
TYPE =
       ∀n:nat.∀m:nat.(eq nat (S (plus n m)) (plus n (S m)))
BODY =
        assume m: nat
        assume n: nat
          we proceed by induction on m to prove eq nat (S (plus m n)) (plus m (S n))
             case O : ⇒
                the thesis becomes eq nat (S (plus O n)) (plus O (S n))
                   by (refl_equal . .)
                   we proved eq nat (S n) (S n)
eq nat (S (plus O n)) (plus O (S n))
             case S : n0:nat ⇒
                the thesis becomes eq nat (S (plus (S n0) n)) (plus (S n0) (S n))
                (H) by induction hypothesis we know eq nat (S (plus n0 n)) (plus n0 (S n))
                   by (f_equal . . . . . H)
                   we proved eq nat (S (S (plus n0 n))) (S (plus n0 (S n)))
eq nat (S (plus (S n0) n)) (plus (S n0) (S n))
          we proved eq nat (S (plus m n)) (plus m (S n))
       we proved ∀m:nat.∀n:nat.(eq nat (S (plus m n)) (plus m (S n)))