X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fgroups.ma;h=699bd73fc3286190a3dbcf9ee3c643b0d8b9ce38;hb=f0cfb75e23d0c1c403c8a67b47be931980f5419f;hp=8353ea67649b26c14f837451568fd11f47e581f5;hpb=8b62b96fea74985e303e093d9b7ead91089c664e;p=helm.git

diff --git a/matita/dama/groups.ma b/matita/dama/groups.ma
index 8353ea676..699bd73fc 100644
--- a/matita/dama/groups.ma
+++ b/matita/dama/groups.ma
@@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/groups/".
 include "higher_order_defs/functions.ma".
 include "nat/nat.ma".
 include "nat/orders.ma".
+include "constructive_connectives.ma".
 
 definition left_neutral \def λC,op.λe:C. ∀x:C. op e x = x.
 
@@ -102,3 +103,38 @@ 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.
+
+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