X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fdama%2Fordered_groups.ma;h=9e72cab5944b57d3ab0d45cd947aa936efb17e9c;hb=2030804124914a9b2155c911d4b835fd67c26d4e;hp=4d2e18e2838b081990d19dab8e8c573137036e93;hpb=47173a864325b6bcaf2d3cb70afcd14be97764ae;p=helm.git

diff --git a/matita/dama/ordered_groups.ma b/matita/dama/ordered_groups.ma
index 4d2e18e28..9e72cab59 100644
--- 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);