rewrite > plus_comm;
rewrite > opp_inverse;
reflexivity.
+qed.
+
+theorem eq_zero_opp_zero: ∀G:abelian_group.0=-0.
+ [ assumption
+ | intros;
+ apply (cancellationlaw ? 0);
+ rewrite < plus_comm in ⊢ (? ? ? %);
+ rewrite > opp_inverse;
+ rewrite > zero_neutral;
+ reflexivity
+ ].
qed.
\ No newline at end of file