rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
rewrite > sym_plus.rewrite < plus_minus_m_m.
reflexivity.
rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
rewrite > sym_plus.rewrite < plus_minus_m_m.
reflexivity.