snapshot

diff --git a/matita/dama/excedence.ma b/matita/dama/excedence.ma
index d91c61170f10862ec14abf62f38ccb26f51e54b4..6d1fc4dd7cf1c292541e963c1b15c051ef564060 100644 (file)
--- a/matita/dama/excedence.ma
+++ b/matita/dama/excedence.ma
@@ -104,8 +104,7 @@ lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
 intros 2 (E x); intro H; cases H (_ ABS); 
 apply (ap_coreflexive ? x ABS);
 qed.
-
-(* 
+ 
 lemma lt_transitive: ∀E.transitive ? (lt E).
 intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz); 
 split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2;
@@ -120,5 +119,3 @@ theorem lt_to_excede: ∀E:excedence.∀a,b:E. (a < b) → (b ≰ a).
 intros (E a b Lab); cases Lab (LEab Aab);
 cases Aab (H H); [cases (LEab H)] fold normalize (b ≰ a); assumption; (* BUG *)  
 qed.
-
-*)
\ No newline at end of file

diff --git a/matita/dama/groups.ma b/matita/dama/groups.ma
index 3e30e04748e84eb9dc937f180db580c21b3524db..da24dadc56ea7d0361f05a23af7dc848969148b5 100644 (file)
--- 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.

diff --git a/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma
index 4d2e18e2838b081990d19dab8e8c573137036e93..9e72cab5944b57d3ab0d45cd947aa936efb17e9c 100644 (file)
--- a/matita/dama/ordered_groups.ma
+++ b/matita/dama/ordered_groups.ma
@@ -14,8 +14,8 @@
 
 set "baseuri" "cic:/matita/ordered_groups/".
 
-include "groups.ma".
 include "ordered_sets.ma".
+include "groups.ma".
 
 record pre_ordered_abelian_group : Type ≝
  { og_abelian_group_: abelian_group;
@@ -41,6 +41,19 @@ record ordered_abelian_group : Type ≝
     is_ordered_abelian_group og_pre_ordered_abelian_group
  }.
 
+lemma le_rewl: ∀E:excedence.∀x,z,y:E. x ≈ y → x ≤ z → y ≤ z.
+intros (E x z y); apply (le_transitive ???? ? H1); 
+clear H1 z; unfold in H; unfold; intro H1; apply H; clear H; 
+lapply ap_cotransitive;  
+intros (G x z y); intro Eyz; 
+
+
+lemma plus_cancr_le: 
+  ∀G:ordered_abelian_group.∀x,y,z:G.x+z ≤ y + z → x ≤ y.
+intros 5 (G x y z L);
+
+ apply L; clear L; elim (exc_cotransitive ???z Exy);
+
 lemma le_zero_x_to_le_opp_x_zero: 
   ∀G:ordered_abelian_group.∀x:G.0 ≤ x → -x ≤ 0.
 intros (G x Px);