From ff19936bfb1e58fea074f71526b4cb7f410d81de Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 6 Dec 2007 11:17:39 +0000 Subject: [PATCH] excede->excess --- helm/software/matita/dama/excess.ma | 2 +- helm/software/matita/dama/ordered_group.ma | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) 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. -- 2.39.2