-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))).
- ]
- ]]
+theorem eq_zero_opp_zero: ∀G:abelian_group.0 ≈ -0. [assumption]
+intro G; apply (plus_cancr ??? 0);
+apply (eq_transitive ?? 0); [apply zero_neutral;]
+apply eq_symmetric; apply opp_inverse;