X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fgroups.ma;h=699bd73fc3286190a3dbcf9ee3c643b0d8b9ce38;hb=50afaf262195266d156f594cff7e92a6e8898b3e;hp=1b39c1518348e7431de23d10ee1d2e6fc3dcf86f;hpb=f1a90ee8745c3fa5324e7a7e8c2f8398483c1ff6;p=helm.git

diff --git a/helm/software/matita/dama/groups.ma b/helm/software/matita/dama/groups.ma
index 1b39c1518..699bd73fc 100644
--- a/helm/software/matita/dama/groups.ma
+++ b/helm/software/matita/dama/groups.ma
@@ -126,4 +126,15 @@ theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x=x.
  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