DEFINITION simpl_plus_r()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(eq nat (plus m n) (plus p n))→(eq nat m p)
BODY =
        assume n: nat
        assume m: nat
        assume p: nat
        suppose H: eq nat (plus m n) (plus p n)
          (h1) 
             by (plus_sym . .)
             we proved eq nat (plus n p) (plus p n)
             by (sym_eq . . . previous)
             we proved eq nat (plus p n) (plus n p)
             by (eq_ind_r . . . previous . H)
eq nat (plus m n) (plus n p)
          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 (plus n m) (plus n p)
          by (simpl_plus_l . . . previous)
          we proved eq nat m p
       we proved ∀n:nat.∀m:nat.∀p:nat.(eq nat (plus m n) (plus p n))→(eq nat m p)