DEFINITION minus_plus_r()
TYPE =
       ∀m:nat.∀n:nat.(eq nat (minus (plus m n) n) m)
BODY =
        assume m: nat
        assume n: nat
          (h1) 
             by (minus_plus . .)
eq nat (minus (plus n m) n) m
          end of h1
          (h2) 
             by (plus_sym . .)
eq nat (plus m n) (plus n m)
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved eq nat (minus (plus m n) n) m
       we proved ∀m:nat.∀n:nat.(eq nat (minus (plus m n) n) m)