DEFINITION plus_assoc_r()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(eq nat (plus (plus n m) p) (plus n (plus m p)))
BODY =
Show proof