-lemma plus_canc: ∀G:abelian_group.∀x,y,z:G. x+y ≈ x+z → y ≈ z.
-intros 6 (G x y z E Ayz); apply E; apply fap_plusl; assumption;
-qed.
+lemma fap_plusr: ∀G:abelian_group.∀x,y,z:G. y # z → y+x # z+x.
+intros (G x y z Ayz); apply (plus_strong_extr ? (-x));
+apply (ap_rewl ??? (y + (x + -x)));
+[1: apply (eq_symmetric ??? (plus_assoc ????));
+|2: apply (ap_rewr ??? (z + (x + -x)));
+ [1: apply (eq_symmetric ??? (plus_assoc ????));
+ |2: apply (ap_rewl ??? (y + (-x+x)) (feq_plusl ???? (plus_comm ???)));
+ apply (ap_rewl ??? (y + 0) (feq_plusl ???? (opp_inverse ??)));
+ apply (ap_rewl ??? (0 + y) (plus_comm ???));
+ apply (ap_rewl ??? y (zero_neutral ??));
+ apply (ap_rewr ??? (z + (-x+x)) (feq_plusl ???? (plus_comm ???)));
+ apply (ap_rewr ??? (z + 0) (feq_plusl ???? (opp_inverse ??)));
+ apply (ap_rewr ??? (0 + z) (plus_comm ???));
+ apply (ap_rewr ??? z (zero_neutral ??));
+ assumption]]
+qed.
+
+lemma plus_cancl: ∀G:abelian_group.∀y,z,x:G. x+y ≈ x+z → y ≈ z.
+intros 6 (G y z x E Ayz); apply E; apply fap_plusl; assumption;
+qed.