bir georganization, most of the structures done

[helm.git] / helm / software / matita / dama / groups.ma

diff --git a/helm/software/matita/dama/groups.ma b/helm/software/matita/dama/groups.ma
index f2b4bd01cfc47198e66f7a52130c38410778b7c9..c00740ee957bd3b433de704cf029d876cc5b6341 100644 (file)
--- 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.