X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fgroups.ma;h=1b39c1518348e7431de23d10ee1d2e6fc3dcf86f;hb=d61b0ec37e7943a058dc9c6381efe49db7eb575f;hp=6d832c208272231be0be1276410fddf5e67c4c88;hpb=bf45bade243d89f2171e76e8eaa9a58489eda45c;p=helm.git

diff --git a/helm/software/matita/dama/groups.ma b/helm/software/matita/dama/groups.ma
index 6d832c208..1b39c1518 100644
--- a/helm/software/matita/dama/groups.ma
+++ b/helm/software/matita/dama/groups.ma
@@ -103,3 +103,27 @@ rewrite > zero_neutral in H1;
 assumption.
 qed.
 
+theorem eq_opp_plus_plus_opp_opp: ∀G:abelian_group.∀x,y:G. -(x+y) = -x + -y.
+ intros;
+ apply (cancellationlaw ? (x+y));
+ rewrite < plus_comm;
+ rewrite > opp_inverse;
+ rewrite > plus_assoc;
+ rewrite > plus_comm in ⊢ (? ? ? (? ? ? (? ? ? %)));
+ rewrite < plus_assoc in ⊢ (? ? ? (? ? ? %));
+ rewrite > plus_comm;
+ rewrite > plus_comm in ⊢ (? ? ? (? ? (? ? % ?) ?));
+ rewrite > opp_inverse;
+ rewrite > zero_neutral;
+ rewrite > opp_inverse;
+ reflexivity.
+qed.
+
+theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x=x.
+ intros;
+ apply (cancellationlaw ? (-x));
+ rewrite > opp_inverse;
+ rewrite > plus_comm;
+ rewrite > opp_inverse;
+ reflexivity.
+qed.
\ No newline at end of file