X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Fordered_group.ma;h=2129aa5c709ea0d33533e06e6ccee229365f2582;hb=c38c15fa800498bcac6230e07a31ed54414a0865;hp=a00b6eb4a365ed2f398419b95475149731499769;hpb=87ed0c3e2ccd74f21f81c2cc9ed2945109bf0a9a;p=helm.git

diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/dama/ordered_group.ma
index a00b6eb4a..2129aa5c7 100644
--- a/helm/software/matita/dama/ordered_group.ma
+++ b/helm/software/matita/dama/ordered_group.ma
@@ -271,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. 
 
@@ -306,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.