sligtly more general results, still to reorganize

diff --git a/helm/software/matita/dama/ordered_divisible_group.ma b/helm/software/matita/dama/ordered_divisible_group.ma
index 0b84d9add806f09caface73ae3800317d672bc2e..805cce9568ad029a230fc4efc79e6081cec6115f 100644 (file)
--- a/helm/software/matita/dama/ordered_divisible_group.ma
+++ b/helm/software/matita/dama/ordered_divisible_group.ma
@@ -103,26 +103,30 @@ apply (plus_cancr_ap ??? 0); assumption;
 qed.
 
 
-lemma foo: ∀G:todgroup.∀x,y:G.∀n.
+lemma lt_suplt: ∀G:todgroup.∀x,y:G.∀n.
 x < y → x\sup (S n) < y\sup (S n).
 intros; elim n; [simplify; apply flt_plusr; assumption]
 simplify; apply (ltplus); [assumption] assumption;
 qed.
 
-lemma foo1: ∀G:todgroup.∀x,y:G.∀n.
-x\sup (S n) < y\sup (S n) → x < y.
+lemma suplt_lt: ∀G:todgroup.∀x,y:G.∀n. x\sup (S n) < y\sup (S n) → x < y.
 intros 4; elim n; [apply (plus_cancr_lt ??? 0); assumption]
 simplify in l; cases (ltplus_orlt ????? l); [assumption]
 apply f; assumption;
 qed.
 
-alias num (instance 0) = "natural number".
-lemma foo3: ∀G:todgroup.∀x,y:G.
-   0<x → 0<y → x\sup 3 ≈ y\sup 4 → y < x.
-intros (G x y H1 H2 H3); apply (foo1 ??? 2); apply (lt_rewr ???? H3);
-simplify; repeat apply flt_plusl; apply (lt_rewr ???? (plus_comm ???));
-apply (lt_rewr ???? (zero_neutral ??)); assumption;
-qed.
+lemma supeqplus_lt: ∀G:todgroup.∀x,y:G.∀n,m.
+   0<x → 0<y → x\sup (S n) ≈ y\sup (S (n+S m)) → y < x.
+intros (G x y n m H1 H2 H3); apply (suplt_lt ??? n); apply (lt_rewr ???? H3);
+clear H3; elim m; [
+  rewrite > sym_plus; simplify; apply (lt_rewl ??? (0+(y+y\sup n))); [
+    apply eq_sym; apply zero_neutral]
+  apply flt_plusr; assumption;]
+apply (lt_transitive ???? l); rewrite > sym_plus; simplify;  
+rewrite > (sym_plus n); simplify; repeat apply flt_plusl;
+apply (lt_rewl ???(0+y\sup(n1+n))); [apply eq_sym; apply zero_neutral]
+apply flt_plusr; assumption;
+qed.  
 
 alias num (instance 0) = "natural number".
 lemma core1: ∀G:todgroup.∀e:G.0<e → e/3 + e/2 + e/2 < e.
@@ -134,8 +138,7 @@ cut (0<w1\sup 3); [2: apply (lt_rewr ???? H2); assumption]
 cut (0<w\sup 4); [2: apply (lt_rewr ???? H1); assumption]
 lapply (gt_pow ??? Hcut) as H4;
 lapply (gt_pow ??? Hcut1) as H5;
-(* elim (eq_le_le ??? H1); elim (eq_le_le ??? H2); *)
-cut (w<w1);[2: apply foo3; try assumption; apply (Eq≈ ? H2 H1);]
+cut (w<w1);[2: apply (supeqplus_lt ??? 2 O); try assumption; apply (Eq≈ ? H2 H1);]
 apply (plus_cancr_lt ??? w1);
 apply (lt_rewl ??? (w+e)); [
   apply (Eq≈ (w+w1\sup 3) ? H2);