+definition ext ≝ λA:apartness.λop:A→A. ∀x,y. x ≈ y → op x ≈ op y.
+
+lemma strong_ext_to_ext: ∀A:apartness.∀op:A→A. strong_ext ? op → ext ? op.
+intros 6 (A op SEop x y Exy); intro Axy; apply Exy; apply SEop; assumption;
+qed.
+
+lemma feq_plusl: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x+y ≈ x+z.
+intros (G x y z Eyz); apply (strong_ext_to_ext ?? (plus_strong_ext ? x));
+assumption;
+qed.
+
+lemma plus_strong_extr: ∀G:abelian_group.∀z:G.strong_ext ? (λx.x + z).
+intros 5 (G z x y A); simplify in A;
+lapply (plus_comm ? z x) as E1; lapply (plus_comm ? z y) as E2;
+lapply (ap_rewl ???? E1 A) as A1; lapply (ap_rewr ???? E2 A1) as A2;
+apply (plus_strong_ext ???? A2);
+qed.
+
+lemma feq_plusr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → y+x ≈ z+x.
+intros (G x y z Eyz); apply (strong_ext_to_ext ?? (plus_strong_extr ? x));
+assumption;
+qed.
+
+lemma fap_plusl: ∀G:abelian_group.∀x,y,z:G. y # z → x+y # x+z.
+intros (G x y z Ayz); apply (plus_strong_ext ? (-x));
+apply (ap_rewl ??? ((-x + x) + y));
+[1: apply plus_assoc;
+|2: apply (ap_rewr ??? ((-x +x) +z));
+ [1: apply plus_assoc;
+ |2: apply (ap_rewl ??? (0 + y));
+ [1: apply (feq_plusr ???? (opp_inverse ??));
+ |2: apply (ap_rewl ???? (zero_neutral ? y)); apply (ap_rewr ??? (0 + z));
+ [1: apply (feq_plusr ???? (opp_inverse ??));
+ |2: apply (ap_rewr ???? (zero_neutral ??)); assumption;]]]]