X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fgroups.ma;h=da24dadc56ea7d0361f05a23af7dc848969148b5;hb=2030804124914a9b2155c911d4b835fd67c26d4e;hp=3e30e04748e84eb9dc937f180db580c21b3524db;hpb=47173a864325b6bcaf2d3cb70afcd14be97764ae;p=helm.git

diff --git a/matita/dama/groups.ma b/matita/dama/groups.ma
index 3e30e0474..da24dadc5 100644
--- a/matita/dama/groups.ma
+++ b/matita/dama/groups.ma
@@ -149,22 +149,12 @@ qed.
 theorem eq_opp_opp_x_x: ∀G:abelian_group.∀x:G.--x ≈ x.
 intros (G x); apply (plus_cancl ??? (-x));
 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).
-  ]
+apply (eq_transitive ?? 0); [apply opp_inverse]
+apply eq_symmetric; apply opp_inverse;
 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))).
-    ]
-  ]]
+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;
 qed.