From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 6 Dec 2007 11:17:39 +0000 (+0000)
Subject: excede->excess
X-Git-Tag: make_still_working~5722
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ff19936bfb1e58fea074f71526b4cb7f410d81de;p=helm.git

excede->excess
---

diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/dama/excess.ma
index 827aaf605..061d2db9b 100644
--- a/helm/software/matita/dama/excess.ma
+++ b/helm/software/matita/dama/excess.ma
@@ -132,7 +132,7 @@ lapply (exc_coreflexive E) as r; unfold coreflexive in r;
 |2: lapply (c ?? x H2) as H3; cases H3 (H4 H4); [right; assumption|cases (Lxy H4)]]
 qed.
 
-theorem lt_to_excede: ∀E:excess.∀a,b:E. (a < b) → (b ≰ a).
+theorem lt_to_excess: ∀E:excess.∀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.
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.