DEFINITION plus_assoc_r()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(eq nat (plus (plus n m) p) (plus n (plus m p)))
BODY =
        assume n: nat
        assume m: nat
        assume p: nat
          by (plus_assoc_l . . .)
          we proved eq nat (plus n (plus m p)) (plus (plus n m) p)
          by (sym_eq . . . previous)
          we proved eq nat (plus (plus n m) p) (plus n (plus m p))
       we proved ∀n:nat.∀m:nat.∀p:nat.(eq nat (plus (plus n m) p) (plus n (plus m p)))