X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_group.ma;h=9a066a80e9a4d62c345515aa0ff948591547b1c3;hb=4bb9fdc4df84b9659ef3850f09e53aa0284a3250;hp=9b70c4f6219298601cb53bbd748047042371d06a;hpb=3a5b9647787e1402f6886d41824f664db290963f;p=helm.git

diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma
index 9b70c4f62..9a066a80e 100644
--- a/helm/software/matita/dama/ordered_group.ma
+++ b/helm/software/matita/dama/ordered_group.ma
@@ -12,14 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/ordered_group/".
+
 
 include "group.ma".
 
 record pogroup_ : Type ≝ { 
   og_abelian_group_: abelian_group;
-  og_excedence:> excedence;
-  og_with: carr og_abelian_group_ = apart_of_excedence og_excedence
+  og_excess:> excess;
+  og_with: carr og_abelian_group_ = apart_of_excess og_excess
 }.
 
 lemma og_abelian_group: pogroup_ → abelian_group.
@@ -181,6 +181,14 @@ apply (lt_rewl ??? x (zero_neutral ??));
 assumption; 
 qed.
 
+lemma lt_opp_x_zero_to_lt_zero_x: 
+  ∀G:pogroup.∀x:G. -x < 0 → 0 < x.
+intros (G x Lx0); apply (plus_cancr_lt ??? (-x));
+apply (lt_rewl ??? (-x) (zero_neutral ??));
+apply (lt_rewr ??? (-x+x) (plus_comm ???));
+apply (lt_rewr ??? 0 (opp_inverse ??));
+assumption; 
+qed.
 
 lemma lt0plus_orlt: 
   ∀G:pogroup. ∀x,y:G. 0 ≤ x → 0 ≤ y → 0 < x + y → 0 < x ∨ 0 < y.
@@ -263,7 +271,7 @@ record togroup : Type ≝ {
 
 lemma lexxyy_lexy: ∀G:togroup. ∀x,y:G. x+x ≤ y+y → x ≤ y.
 intros (G x y H); intro H1; lapply (tog_total ??? H1) as H2;
-lapply (ltxy_ltyyxx ??? H2) as H3; lapply (lt_to_excede ??? H3) as H4;
+lapply (ltxy_ltyyxx ??? H2) as H3; lapply (lt_to_excess ??? H3) as H4;
 cases (H H4);
 qed. 
 
@@ -298,16 +306,16 @@ intros (G a b c d H1 H2); intro H3; cases (excplus_orexc ????? H3);
 qed.  
 
 lemma leplus_lt_le: ∀G:togroup.∀x,y:G. 0 ≤ x + y → x < 0 → 0 ≤ y.
-intros; intro; apply H; lapply (lt_to_excede ??? l);
+intros; intro; apply H; lapply (lt_to_excess ??? l);
 lapply (tog_total ??? e);
 lapply (tog_total ??? Hletin);
 lapply (ltplus ????? Hletin2 Hletin1);
 apply (exc_rewl ??? (0+0)); [apply eq_sym; apply zero_neutral]
-apply lt_to_excede; assumption;
+apply lt_to_excess; assumption;
 qed. 
 
 lemma ltplus_orlt: ∀G:togroup.∀a,b,c,d:G. a+c < b + d →  a < b ∨ c < d.
-intros (G a b c d H1 H2); lapply (lt_to_excede ??? H1);
+intros (G a b c d H1 H2); lapply (lt_to_excess ??? H1);
 cases (excplus_orexc ????? Hletin); [left|right] apply tog_total; assumption;
 qed.