Finished Rplus_assoc proof

Also replaced first order with faster tactics