X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fgroups.ma;h=c00740ee957bd3b433de704cf029d876cc5b6341;hb=9791cd146bc0b8df953aee7bb8a3df60553b530c;hp=f2b4bd01cfc47198e66f7a52130c38410778b7c9;hpb=20d600f225a0994c607b23226578078eb6b79bbe;p=helm.git

diff --git a/helm/software/matita/dama/groups.ma b/helm/software/matita/dama/groups.ma
index f2b4bd01c..c00740ee9 100644
--- a/helm/software/matita/dama/groups.ma
+++ b/helm/software/matita/dama/groups.ma
@@ -205,3 +205,25 @@ compose feq_plusl with feq_opp(H); apply H; assumption;
 qed.
 
 coercion cic:/matita/groups/eq_opp_plusl.con nocomposites.
+
+lemma plus_cancr_ap: ∀G:abelian_group.∀x,y,z:G. x+z # y+z → x # y.
+intros (G x y z H); lapply (fap_plusr ? (-z) ?? H) as H1; clear H;
+lapply (ap_rewl ? (x + (z + -z)) ?? (plus_assoc ? x z (-z)) H1) as H2; clear H1;
+lapply (ap_rewl ? (x + (-z + z)) ?? (plus_comm ?z (-z)) H2) as H1; clear H2;
+lapply (ap_rewl ? (x + 0) ?? (opp_inverse ?z) H1) as H2; clear H1;
+lapply (ap_rewl ? (0+x) ?? (plus_comm ?x 0) H2) as H1; clear H2;
+lapply (ap_rewl ? x ?? (zero_neutral ?x) H1) as H2; clear H1;
+lapply (ap_rewr ? (y + (z + -z)) ?? (plus_assoc ? y z (-z)) H2) as H3;
+lapply (ap_rewr ? (y + (-z + z)) ?? (plus_comm ?z (-z)) H3) as H4;
+lapply (ap_rewr ? (y + 0) ?? (opp_inverse ?z) H4) as H5;
+lapply (ap_rewr ? (0+y) ?? (plus_comm ?y 0) H5) as H6;
+lapply (ap_rewr ? y ?? (zero_neutral ?y) H6);
+assumption;
+qed.
+
+lemma pluc_cancl_ap: ∀G:abelian_group.∀x,y,z:G. z+x # z+y → x # y.
+intros (G x y z H); apply (plus_cancr_ap ??? z);
+apply (ap_rewl ???? (plus_comm ???)); 
+apply (ap_rewr ???? (plus_comm ???));
+assumption;
+qed.