-apply (eq_transitive ?? (--x + -x)); [apply plus_comm]
-apply (eq_transitive (carr G) (plus G (opp G (opp G x)) (opp G x)) (zero G) (plus G (opp G x) x) ? ?);
- [apply (opp_inverse G (opp G x)).
- |apply (eq_symmetric (carr G) (plus G (opp G x) x) (zero G) ?).
- apply (opp_inverse G x).
- ]
-qed.
-
-theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0.
- [ assumption
- | intros;
-apply (eq_transitive (carr G) (zero G) (plus G (opp G (zero G)) (zero G)) (opp G (zero G)) ? ?);
- [apply (eq_symmetric (carr G) (plus G (opp G (zero G)) (zero G)) (zero G) ?).
- apply (opp_inverse G (zero G)).
- |apply (eq_transitive (carr G) (plus G (opp G (zero G)) (zero G)) (plus G (zero G) (opp G (zero G))) (opp G (zero G)) ? ?);
- [apply (plus_comm G (opp G (zero G)) (zero G)).
- |apply (zero_neutral G (opp G (zero G))).
- ]
- ]]
+apply (eq_trans ?? (--x + -x)); [apply plus_comm]
+apply (eq_trans ?? 0); [apply opp_inverse]
+apply eq_sym; apply opp_inverse;
+qed.
+
+theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0. [assumption]
+intro G; apply (plus_cancr ??? 0);
+apply (eq_trans ?? 0); [apply zero_neutral;]
+apply eq_sym; apply opp_inverse;
+qed.
+
+lemma feq_oppr: ∀G:abelian_group.∀x,y,z:G. y ≈ z → x ≈ -y → x ≈ -z.
+intros (G x y z H1 H2); apply (plus_cancr ??? z);
+apply (eq_trans ?? 0 ?? (opp_inverse ?z));
+apply (eq_trans ?? (-y + z) ? H2);
+apply (eq_trans ?? (-y + y) ? H1);
+apply (eq_trans ?? 0 ? (opp_inverse ??));
+apply eq_reflexive;
+qed.
+
+lemma feq_oppl: ∀G:abelian_group.∀x,y,z:G. y ≈ z → -y ≈ x → -z ≈ x.
+intros (G x y z H1 H2); apply eq_sym; apply (feq_oppr ??y);
+[2:apply eq_sym] assumption;
+qed.
+
+lemma feq_opp: ∀G:abelian_group.∀x,y:G. x ≈ y → -x ≈ -y.
+intros (G x y H); apply (feq_oppl ??y ? H); apply eq_reflexive;