cleanup

[helm.git] / matita / dama / groups.ma

diff --git a/matita/dama/groups.ma b/matita/dama/groups.ma
index 3e30e04748e84eb9dc937f180db580c21b3524db..f676258172ad7f298aab4d25b20a2ed4eae0ebe7 100644 (file)
--- a/matita/dama/groups.ma
+++ b/matita/dama/groups.ma
@@ -42,7 +42,7 @@ record abelian_group : Type ≝
    opp_inverse: left_inverse ? plus zero opp;
    plus_strong_ext: ∀z.strong_ext ? (plus z)  
 }.
- 
+
 notation "0" with precedence 89 for @{ 'zero }.
 
 interpretation "Abelian group zero" 'zero =
@@ -59,16 +59,6 @@ definition minus ≝
 
 interpretation "Abelian group minus" 'minus a b =
  (cic:/matita/groups/minus.con _ a b).
- 
-lemma ap_rewl: ∀A:apartness.∀x,z,y:A. x ≈ y → y # z → x # z.
-intros (A x z y Exy Ayz); cases (ap_cotransitive ???x Ayz); [2:assumption]
-cases (Exy (ap_symmetric ??? a));
-qed.
-  
-lemma ap_rewr: ∀A:apartness.∀x,z,y:A. x ≈ y → z # y → z # x.
-intros (A x z y Exy Azy); apply ap_symmetric; apply (ap_rewl ???? Exy);
-apply ap_symmetric; assumption;
-qed.
 
 definition ext ≝ λA:apartness.λop:A→A. ∀x,y. x ≈ y → op x ≈ op y.
 
@@ -80,6 +70,8 @@ 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.  
+
+coercion cic:/matita/groups/feq_plusl.con.
    
 lemma plus_strong_extr: ∀G:abelian_group.∀z:G.strong_ext ? (λx.x + z).
 intros 5 (G z x y A); simplify in A;
@@ -93,6 +85,8 @@ intros (G x y z Eyz); apply (strong_ext_to_ext ?? (plus_strong_extr ? x));
 assumption;
 qed.   
    
+coercion cic:/matita/groups/feq_plusr.con.   
+   
 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));
@@ -106,6 +100,8 @@ apply (ap_rewl ??? ((-x + x) + y));
             |2: apply (ap_rewr ???? (zero_neutral ??)); 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)));
@@ -149,22 +145,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.