DEFINITION plus_Snm_nSm()
TYPE =
       ∀n:nat.∀m:nat.(eq nat (plus (S n) m) (plus n (S m)))
BODY =
        assume n: nat
        assume m: nat
          (h1) 
             (h1) 
                by (refl_equal . .)
                we proved eq nat (plus (S m) n) (plus (S m) n)
eq nat (S (plus m n)) (plus (S m) n)
             end of h1
             (h2) 
                by (plus_sym . .)
eq nat (plus n (S m)) (plus (S m) n)
             end of h2
             by (eq_ind_r . . . h1 . h2)
eq nat (S (plus m n)) (plus n (S m))
          end of h1
          (h2) 
             by (plus_sym . .)
eq nat (plus n m) (plus m n)
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved eq nat (S (plus n m)) (plus n (S m))
          that is equivalent to eq nat (plus (S n) m) (plus n (S m))
       we proved ∀n:nat.∀m:nat.(eq nat (plus (S n) m) (plus n (S m)))