From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 4 Dec 2007 09:55:44 +0000 (+0000)
Subject: sandwitch theorem done
X-Git-Tag: make_still_working~5739
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=11f667afbb87725dd5e243d4b3717d19f584a481;p=helm.git

sandwitch theorem done
---

diff --git a/helm/software/matita/dama/divisible_group.ma b/helm/software/matita/dama/divisible_group.ma
index 5c7025a9c..7d2eeed45 100644
--- a/helm/software/matita/dama/divisible_group.ma
+++ b/helm/software/matita/dama/divisible_group.ma
@@ -17,15 +17,15 @@ set "baseuri" "cic:/matita/divisible_group/".
 include "nat/orders.ma".
 include "group.ma".
 
-let rec pow (G : abelian_group) (x : G) (n : nat) on n : G ≝
-  match n with [ O ⇒ 0 | S m ⇒ x + pow ? x m].
+let rec gpow (G : abelian_group) (x : G) (n : nat) on n : G ≝
+  match n with [ O ⇒ 0 | S m ⇒ x + gpow ? x m].
   
-interpretation "abelian group pow" 'exp x n =
-  (cic:/matita/divisible_group/pow.con _ x n).
+interpretation "additive abelian group pow" 'times n x =
+  (cic:/matita/divisible_group/gpow.con _ x n).
   
 record dgroup : Type ≝ {
   dg_carr:> abelian_group;
-  dg_prop: ∀x:dg_carr.∀n:nat.∃y.pow ? y (S n) ≈ x
+  dg_prop: ∀x:dg_carr.∀n:nat.∃y.S n * y ≈ x
 }.
 
 lemma divide: ∀G:dgroup.G → nat → G.
@@ -36,15 +36,15 @@ interpretation "divisible group divide" 'divide x n =
   (cic:/matita/divisible_group/divide.con _ x n).
 
 lemma divide_divides: 
-  ∀G:dgroup.∀x:G.∀n. pow ? (x / n) (S n) ≈ x.
+  ∀G:dgroup.∀x:G.∀n. S n * (x / n) ≈ x.
 intro G; cases G; unfold divide; intros (x n); simplify;
 cases (f x n); simplify; exact H;
 qed.  
   
-lemma feq_pow: ∀G:dgroup.∀x,y:G.∀n.x≈y → pow ? x n ≈ pow ? y n.
+lemma feq_pow: ∀G:dgroup.∀x,y:G.∀n.x≈y → n * x ≈ n * y.
 intros (G x y n H); elim n; [apply eq_reflexive]
-simplify; apply (Eq≈ (x + (pow ? y n1)) H1);
-apply (Eq≈ (y+pow ? y n1) H (eq_reflexive ??));
+simplify; apply (Eq≈ (x + (n1 * y)) H1);
+apply (Eq≈ (y+n1*y) H (eq_reflexive ??));
 qed.
 
 lemma div1: ∀G:dgroup.∀x:G.x/O ≈ x.
@@ -53,3 +53,33 @@ cases (f x O); simplify; simplify in H; intro; apply H;
 apply (ap_rewl ???? (plus_comm ???));
 apply (ap_rewl ???w (zero_neutral ??)); assumption;
 qed.
+
+lemma appow_ap: ∀G:dgroup.∀x,y:G.∀n.S n * x # S n * y → x # y.
+intros 4 (G x y n); elim n; [2:
+  simplify in a;
+  cases (applus ????? a); [assumption]
+  apply f; assumption;]
+apply (plus_cancr_ap ??? 0); assumption;
+qed.
+
+lemma pluspow: ∀G:dgroup.∀x,y:G.∀n.n * (x+y) ≈ n * x + n * y.
+intros (G x y n); elim n; [
+  simplify; apply (Eq≈ 0 ? (zero_neutral ? 0)); apply eq_reflexive]
+simplify; apply eq_sym; apply (Eq≈ (x+y+(n1*x+n1*y))); [
+  apply (Eq≈ (x+(n1*x+(y+(n1*y))))); [
+    apply eq_sym; apply plus_assoc;]
+  apply (Eq≈ (x+((n1*x+y+(n1*y))))); [
+    apply feq_plusl; apply plus_assoc;]
+  apply (Eq≈ (x+(y+n1*x+n1*y))); [
+    apply feq_plusl; apply feq_plusr; apply plus_comm;] 
+  apply (Eq≈ (x+(y+(n1*x+n1*y)))); [
+    apply feq_plusl; apply eq_sym; apply plus_assoc;]
+  apply plus_assoc;]
+apply feq_plusl; apply eq_sym; assumption;
+qed. 
+
+lemma powzero: ∀G:dgroup.∀n.n*0 ≈ 0. [2: apply dg_carr; apply G]
+intros; elim n; [simplify; apply eq_reflexive]
+simplify; apply (Eq≈ ? (zero_neutral ??)); assumption; 
+qed.
+
diff --git a/helm/software/matita/dama/group.ma b/helm/software/matita/dama/group.ma
index a04cd3bcc..b298e82e0 100644
--- a/helm/software/matita/dama/group.ma
+++ b/helm/software/matita/dama/group.ma
@@ -138,6 +138,12 @@ apply (ap_rewl ??? (y + (x + -x)));
         apply (ap_rewr ??? z (zero_neutral ??));
         assumption]]
 qed.
+
+lemma applus: ∀E:abelian_group.∀x,a,y,b:E.x + a # y + b → x # y ∨ a # b.
+intros; cases (ap_cotransitive ??? (y+a) a1); [left|right]
+[apply (plus_cancr_ap ??? a)|apply (plus_cancl_ap ??? y)]
+assumption;
+qed.
     
 lemma plus_cancl: ∀G:abelian_group.∀y,z,x:G. x+y ≈ x+z → y ≈ z. 
 intros 6 (G y z x E Ayz); apply E; apply fap_plusl; assumption;
diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/dama/metric_lattice.ma
index be9412087..cca643098 100644
--- a/helm/software/matita/dama/metric_lattice.ma
+++ b/helm/software/matita/dama/metric_lattice.ma
@@ -89,102 +89,18 @@ cut ( δx y+ δy z ≈ δ(y∨x) (y∨z)+ δ(y∧x) (y∧z)); [
   apply (le_rewr ??? (δx y+ δy z)); [assumption] apply le_reflexive]
 lapply (le_to_eqm ??? Lxy) as Dxm; lapply (le_to_eqm ??? Lyz) as Dym;
 lapply (le_to_eqj ??? Lxy) as Dxj; lapply (le_to_eqj ??? Lyz) as Dyj; clear Lxy Lyz;
-apply (Eq≈ (δ(x∧y) y + δy z)); [apply feq_plusr; apply (meq_l ????? Dxm);]
-apply (Eq≈ (δ(x∧y) (y∧z) + δy z)); [apply feq_plusr; apply (meq_r ????? Dym);]
-apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) z)); [apply feq_plusl; apply (meq_l ????? Dxj);]
-apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z))); [apply feq_plusl; apply (meq_r ????? Dyj);]
+apply (Eq≈ (δ(x∧y) y + δy z) (meq_l ????? Dxm));
+apply (Eq≈ (δ(x∧y) (y∧z) + δy z) (meq_r ????? Dym));
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) z) (meq_l ????? Dxj));
+apply (Eq≈ (δ(x∧y) (y∧z) + δ(x∨y) (y∨z)) (meq_r ????? Dyj));
 apply (Eq≈ ? (plus_comm ???));
-apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z))); [apply feq_plusr; apply (meq_l ????? (join_comm ???));]
+apply (Eq≈ (δ(y∨x) (y∨z)+ δ(x∧y) (y∧z)) (meq_l ????? (join_comm ?x y)));
 apply feq_plusl;
-apply (Eq≈ (δ(y∧x) (y∧z))); [apply (meq_l ????? (meet_comm ???));]
+apply (Eq≈ (δ(y∧x) (y∧z)) (meq_l ????? (meet_comm ?x y)));
 apply eq_reflexive;   
 qed.  
 
-include "sequence.ma".
-include "nat/plus.ma".
 
-lemma ltwl: ∀a,b,c:nat. b + a < c → a < c.
-intros 3 (x y z); elim y (H z IH H); [apply H]
-apply IH; apply lt_S_to_lt; apply H;
-qed.
-
-lemma ltwr: ∀a,b,c:nat. a + b < c → a < c.
-intros 3 (x y z); rewrite > sym_plus; apply ltwl;
-qed. 
-
-
-definition d2s ≝ 
-  λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
-(*
-notation "s ⇝ 'Zero'" non associative with precedence 50 for @{'tends0 $s }.
-  
-interpretation "tends to" 'tends s x = 
-  (cic:/matita/sequence/tends0.con _ s).    
-*)
-
-alias symbol "leq" = "ordered sets less or equal than".
-alias symbol "and" = "constructive and".
-alias symbol "exists" = "constructive exists (Type)".
-theorem carabinieri:
-  ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.
-    (∀n. (an n ≤ xn n) ∧ (xn n ≤ bn n)) →
-    ∀x:ml. tends0 ? (d2s ? ml an x) → tends0 ? (d2s ? ml bn x) →
-    tends0 ? (d2s ? ml xn x).
-intros (R ml an bn xn H x Ha Hb); unfold tends0 in Ha Hb ⊢ %. unfold d2s in Ha Hb ⊢ %.
-intros (e He);
-alias num (instance 0) = "natural number".
-elim (Ha (e/2) (divide_preserves_lt ??? He)) (n1 H1); clear Ha; 
-elim (Hb (e/3) (divide_preserves_lt ??? He)) (n2 H2); clear Hb;
-constructor 1; [apply (n1 + n2);] intros (n3 Hn3);
-lapply (ltwr ??? Hn3) as Hn1n3; lapply (ltwl ??? Hn3) as Hn2n3;
-elim (H1 ? Hn1n3) (H3 H4); elim (H2 ? Hn2n3) (H5 H6); clear Hn1n3 Hn2n3;
-elim (H n3) (H7 H8); clear H H1 H2; 
-lapply (le_to_eqm ??? H7) as Dxm; lapply (le_to_eqj ??? H7) as Dym;
-(* the main step *)
-cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x); [2:
-  apply (le_transitive ???? (mtineq ???? (an n3)));
-  lapply (le_mtri ????? H7 H8);
-  lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? Hletin);
-  cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))); [2:
-    apply (Eq≈  (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
-    apply (Eq≈  (δ(an n3) (xn n3) + 0) ? (plus_comm ???));
-    apply (Eq≈  (δ(an n3) (xn n3) +  (-δ(xn n3) (bn n3) +  δ(xn n3) (bn n3))) ? (opp_inverse ??));
-    apply (Eq≈  (δ(an n3) (xn n3) +  (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3))));
-    apply (Eq≈  ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear Hletin1;
-  apply (le_rewl ???  ( δ(an n3) (xn n3)+ δ(an n3) x));[
-    apply feq_plusr; apply msymmetric;]
-  apply (le_rewl ???  (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x));[
-    apply feq_plusr; assumption;]
-  clear Hcut Hletin Dym Dxm H8 H7 H6 H5 H4 H3;
-  apply (le_rewl ??? (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x));[
-    apply feq_plusr; apply plus_comm;]
-  apply (le_rewl ??? (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????));
-  apply (le_rewl ??? ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???));
-  apply lew_opp; [apply mpositive] apply fle_plusr;
-  apply (le_rewr ???? (plus_comm ???));
-  apply (le_rewr ??? ( δ(an n3) x+ δx (bn n3)) (msymmetric ????));
-  apply mtineq;]
-split; [
-  apply (lt_le_transitive ????? (mpositive ????));
-  split; elim He; [apply  le_zero_x_to_le_opp_x_zero; assumption;]
-  cases t1; [ 
-    left; apply exc_zero_opp_x_to_exc_x_zero;
-    apply (Ex≫ ? (eq_opp_opp_x_x ??));assumption;]
-  right;  apply exc_opp_x_zero_to_exc_zero_x;
-  apply (Ex≪ ? (eq_opp_opp_x_x ??)); assumption;]
-clear Dxm Dym H7 H8 Hn3 H5 H3 n1 n2;
-apply (le_lt_transitive ???? ? (core1 ?? He));
-apply (le_transitive ???? Hcut);
-apply (le_transitive ??  (e/3+ δ(an n3) x+ δ(an n3) x)); [
-  repeat apply fle_plusr; cases H6; assumption;]
-apply (le_transitive ??  (e/3+ e/2 + δ(an n3) x)); [
-  apply fle_plusr; apply fle_plusl; cases H4; assumption;]
-apply (le_transitive ??  (e/3+ e/2 + e/2)); [
-  apply fle_plusl; cases H4; assumption;]
-apply le_reflexive;
-qed.
-
-  
 (* 3.17 conclusione: δ x y ≈ 0 *)
 (* 3.20 conclusione: δ x y ≈ 0 *)
 (* 3.21 sup forte
diff --git a/helm/software/matita/dama/ordered_divisible_group.ma b/helm/software/matita/dama/ordered_divisible_group.ma
index 805cce956..cae552114 100644
--- a/helm/software/matita/dama/ordered_divisible_group.ma
+++ b/helm/software/matita/dama/ordered_divisible_group.ma
@@ -32,123 +32,44 @@ qed.
 
 coercion cic:/matita/ordered_divisible_group/todg_division.con.
 
-lemma pow_lt: ∀G:todgroup.∀x:G.∀n.0 < x → 0 < x + pow ? x n.
-intros (G x n H); elim n; [
-  simplify; apply (lt_rewr ???? (plus_comm ???)); 
-  apply (lt_rewr ???x (zero_neutral ??)); assumption]
-simplify; apply (lt_transitive ?? (x+(x)\sup(n1))); [assumption]
-apply flt_plusl; apply (lt_rewr ???? (plus_comm ???));
-apply (lt_rewl ??? (0 + (x \sup n1)) (eq_sym ??? (zero_neutral ??)));
-apply (lt_rewl ???? (plus_comm ???));
-apply flt_plusl; assumption;
-qed.
-
-lemma pow_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ pow ? x n.
+lemma pow_ge: ∀G:todgroup.∀x:G.∀n.0 ≤ x → 0 ≤ n * x.
 intros (G x n); elim n; simplify; [apply le_reflexive]
 apply (le_transitive ???? H1); 
-apply (le_rewl ??? (0+(x\sup n1)) (zero_neutral ??));
+apply (le_rewl ??? (0+(n1*x)) (zero_neutral ??));
 apply fle_plusr; assumption;
 qed. 
 
-lemma gt_pow: ∀G:todgroup.∀x:G.∀n.0 < pow ? x n → 0 < x.
-intros 3; elim n; [
-  simplify in l; cases (lt_coreflexive ?? l);]
-simplify in l; 
-cut (0+0<x+(x)\sup(n1));[2:
-  apply (lt_rewl ??? 0 (zero_neutral ??)); assumption].
-cases (ltplus_orlt ????? Hcut); [assumption]
-apply f; assumption;
-qed.
-
-lemma gt_pow2: ∀G:dgroup.∀x,y:G.∀n.pow ? x n + pow ? y n ≈ pow ? (x+y) n.
-intros (G x y n); elim n; [apply (Eq≈ 0 (zero_neutral ??)); apply eq_reflexive]
-simplify; apply (Eq≈ (x+y+((x)\sup(n1)+(y)\sup(n1)))); [
-  apply (Eq≈ (x+((x)\sup(n1)+(y+(y)\sup(n1))))); [
-    apply eq_sym; apply plus_assoc;]
-  apply (Eq≈ (x+((x)\sup(n1)+y+(y)\sup(n1)))); [
-    apply feq_plusl; apply plus_assoc;]
-  apply (Eq≈ (x+(y+(x)\sup(n1)+(y)\sup(n1)))); [
-    apply feq_plusl; apply feq_plusr; apply plus_comm;] 
-  apply (Eq≈ (x+(y+((x)\sup(n1)+(y)\sup(n1))))); [
-    apply feq_plusl; apply eq_sym; apply plus_assoc;]
-  apply plus_assoc;]
-apply feq_plusl; assumption;
-qed. 
-  
-lemma xxxx: ∀E:abelian_group.∀x,a,y,b:E.x + a # y + b → x # y ∨ a # b.
-intros; cases (ap_cotransitive ??? (y+a) a1); [left|right]
-[apply (plus_cancr_ap ??? a)|apply (plus_cancl_ap ??? y)]
-assumption;
-qed.
-   
-lemma pow_gt0: ∀G:todgroup.∀y:G.∀n.0 < y → 0 < pow ? y (S n).
-intros (G y n H); elim n; [apply (lt_rewr ??? (0+y) (plus_comm ???)); apply (lt_rewr ??? y (zero_neutral ??)); apply H]
-simplify; apply (lt_rewl ? 0 ? (0+0) (zero_neutral ? 0));
-apply ltplus; assumption;
-qed.
-
-lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0<e → 0 < e/n.
-intros; elim n; [apply (lt_rewr ???? (div1 ??));assumption]
-unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
-apply (gt_pow ?? (S (S n1))); apply (lt_rewr ???? f); assumption;
-qed.
-
-
-lemma bar1: ∀G:togroup.∀x,y:G.∀n.pow ? x (S n) # pow ? y (S n) → x # y.
-intros 4 (G x y n); elim n; [2:
-  simplify in a;
-  cases (xxxx ????? a); [assumption]
-  apply f; assumption;]
-apply (plus_cancr_ap ??? 0); assumption;
-qed.
-
-
-lemma lt_suplt: ∀G:todgroup.∀x,y:G.∀n.
-x < y → x\sup (S n) < y\sup (S n).
+lemma lt_ltpow: ∀G:todgroup.∀x,y:G.∀n. x < y → S n * x < S n * y.
 intros; elim n; [simplify; apply flt_plusr; assumption]
 simplify; apply (ltplus); [assumption] assumption;
 qed.
 
-lemma suplt_lt: ∀G:todgroup.∀x,y:G.∀n. x\sup (S n) < y\sup (S n) → x < y.
+lemma ltpow_lt: ∀G:todgroup.∀x,y:G.∀n. S n * x < S n * y → x < y.
 intros 4; elim n; [apply (plus_cancr_lt ??? 0); assumption]
 simplify in l; cases (ltplus_orlt ????? l); [assumption]
 apply f; 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);
+lemma divide_preserves_lt: ∀G:todgroup.∀e:G.∀n.0<e → 0 < e/n.
+intros; elim n; [apply (lt_rewr ???? (div1 ??));assumption]
+unfold divide; elim (dg_prop G e (S n1)); simplify; simplify in f;
+apply (ltpow_lt ??? (S n1)); simplify; apply (lt_rewr ???? f);
+apply (lt_rewl ???? (zero_neutral ??)); 
+apply (lt_rewl ???? (zero_neutral ??)); 
+apply (lt_rewl ???? (powzero ?n1));
+assumption;
+qed.
+
+lemma poweqplus_lt: ∀G:todgroup.∀x,y:G.∀n,m.
+   0<x → 0<y → S n * x ≈ S (n + S m) * y → y < x.
+intros (G x y n m H1 H2 H3); apply (ltpow_lt ??? n); apply (lt_rewr ???? H3);
 clear H3; elim m; [
-  rewrite > sym_plus; simplify; apply (lt_rewl ??? (0+(y+y\sup n))); [
+  rewrite > sym_plus; simplify; apply (lt_rewl ??? (0+(y+n*y))); [
     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 (lt_rewl ???(0+(n1+n)*y)); [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.
-intro G; cases G; unfold divide; intro e;
-cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 3) 0;
-cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 2) 0; simplify;
-intro H3;
-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;
-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);
-  apply (Eq≈ (w+w1+(w1+w1)) (plus_assoc ??w1 w1));
-  apply (Eq≈ (w+(w1+(w1+w1))) (plus_assoc ?w w1 ?));
-  simplify; repeat apply feq_plusl; apply eq_sym; 
-  apply (Eq≈ ? (plus_comm ???)); apply zero_neutral;]
-apply (lt_rewl ???? (plus_comm ???));
-apply flt_plusl; assumption;
-qed.
-  
-  
-
diff --git a/helm/software/matita/dama/premetric_lattice.ma b/helm/software/matita/dama/premetric_lattice.ma
index 42d00fd26..d985ec24f 100644
--- a/helm/software/matita/dama/premetric_lattice.ma
+++ b/helm/software/matita/dama/premetric_lattice.ma
@@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/premetric_lattice/".
 
 include "metric_space.ma".
 
-record premetric_lattice_ (R : ogroup) : Type ≝ {
+record premetric_lattice_ (R : todgroup) : Type ≝ {
   pml_carr:> metric_space R;
   meet: pml_carr → pml_carr → pml_carr;
   join: pml_carr → pml_carr → pml_carr
@@ -28,7 +28,7 @@ interpretation "valued lattice meet" 'and a b =
 interpretation "valued lattice join" 'or a b =
  (cic:/matita/premetric_lattice/join.con _ _ a b).
  
-record premetric_lattice_props (R : ogroup) (ml : premetric_lattice_ R) : Prop ≝ {
+record premetric_lattice_props (R : todgroup) (ml : premetric_lattice_ R) : Prop ≝ {
   prop1a: ∀a : ml.δ (a ∧ a) a ≈ 0;
   prop1b: ∀a : ml.δ (a ∨ a) a ≈ 0;
   prop2a: ∀a,b: ml. δ (a ∨ b) (b ∨ a) ≈ 0;
@@ -40,14 +40,14 @@ record premetric_lattice_props (R : ogroup) (ml : premetric_lattice_ R) : Prop 
   prop5: ∀a,b,c: ml. δ (a ∨ b) (a ∨ c) + δ (a ∧ b) (a ∧ c) ≤ δ b c
 }.
 
-record pmlattice (R : ogroup) : Type ≝ {
+record pmlattice (R : todgroup) : Type ≝ {
   carr :> premetric_lattice_ R;
   ispremetriclattice:> premetric_lattice_props R carr
 }.
   
 include "lattice.ma".
 
-lemma lattice_of_pmlattice: ∀R: ogroup. pmlattice R → lattice.
+lemma lattice_of_pmlattice: ∀R: todgroup. pmlattice R → lattice.
 intros (R pml); apply (mk_lattice (apart_of_metric_space ? pml));
 [apply (join ? pml)|apply (meet ? pml)
 |3,4,5,6,7,8,9,10: intros (x y z); whd; intro H; whd in H; cases H (LE AP);]
diff --git a/helm/software/matita/dama/sandwich.ma b/helm/software/matita/dama/sandwich.ma
new file mode 100644
index 000000000..c83136c77
--- /dev/null
+++ b/helm/software/matita/dama/sandwich.ma
@@ -0,0 +1,123 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/sandwich/".
+
+include "nat/plus.ma".
+include "nat/orders.ma".
+
+lemma ltwl: ∀a,b,c:nat. b + a < c → a < c.
+intros 3 (x y z); elim y (H z IH H); [apply H]
+apply IH; apply lt_S_to_lt; apply H;
+qed.
+
+lemma ltwr: ∀a,b,c:nat. a + b < c → a < c.
+intros 3 (x y z); rewrite > sym_plus; apply ltwl;
+qed. 
+
+include "sequence.ma".
+include "metric_lattice.ma".
+
+lemma sandwich_ineq: ∀G:todgroup.∀e:G.0<e → e/3 + e/2 + e/2 < e.
+intro G; cases G; unfold divide; intro e;
+alias num (instance 0) = "natural number".
+cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 3) 0;
+cases (dg_prop (mk_todgroup todg_order todg_division_ H) e 2) 0; simplify;
+intro H3;
+cut (0<w1) as H4; [2: 
+  apply (ltpow_lt ??? 2); apply (lt_rewr ???? H2);
+  apply (lt_rewl ???? (powzero ? 3)); assumption]
+cut (0<w) as H5; [2:
+  apply (ltpow_lt ??? 3); apply (lt_rewr ???? H1);
+  apply (lt_rewl ???? (powzero ? 4)); assumption]
+cut (w<w1) as H6; [2: 
+  apply (poweqplus_lt ??? 2 O); try assumption; apply (Eq≈ ? H2 H1);]
+apply (plus_cancr_lt ??? w1);
+apply (lt_rewl ??? (w+e)); [
+  apply (Eq≈ (w+3*w1) ? H2);
+  apply (Eq≈ (w+w1+(w1+w1)) (plus_assoc ??w1 w1));
+  apply (Eq≈ (w+(w1+(w1+w1))) (plus_assoc ?w w1 ?));
+  simplify; repeat apply feq_plusl; apply eq_sym; 
+  apply (Eq≈ ? (plus_comm ???)); apply zero_neutral;]
+apply (lt_rewl ???? (plus_comm ???));
+apply flt_plusl; assumption;
+qed.
+
+definition d2s ≝ 
+  λR.λml:mlattice R.λs:sequence ml.λk.λn. δ (s n) k.
+
+notation "s ⇝ x" non associative with precedence 50 for @{'tends $s $x}.
+  
+interpretation "tends to" 'tends s x = 
+  (cic:/matita/sequence/tends0.con _ (cic:/matita/sandwich/d2s.con _ _ s x)).
+    
+alias symbol "and" = "constructive and".
+theorem sandwich:
+  ∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
+    (∀n. (an n ≤ xn n) ∧ (xn n ≤ bn n)) → 
+    an ⇝ x → 
+    bn ⇝ x →
+    xn ⇝ x.
+intros (R ml an bn xn x H Ha Hb); unfold tends0 in Ha Hb ⊢ %. unfold d2s in Ha Hb ⊢ %.
+intros (e He);
+elim (Ha (e/2) (divide_preserves_lt ??? He)) (n1 H1); clear Ha; 
+elim (Hb (e/3) (divide_preserves_lt ??? He)) (n2 H2); clear Hb;
+constructor 1; [apply (n1 + n2);] intros (n3 Hn3);
+lapply (ltwr ??? Hn3) as Hn1n3; lapply (ltwl ??? Hn3) as Hn2n3;
+elim (H1 ? Hn1n3) (H3 H4); elim (H2 ? Hn2n3) (H5 H6); clear Hn1n3 Hn2n3;
+elim (H n3) (H7 H8); clear H H1 H2; 
+lapply (le_to_eqm ??? H7) as Dxm; lapply (le_to_eqj ??? H7) as Dym;
+(* the main step *)
+cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x); [2:
+  apply (le_transitive ???? (mtineq ???? (an n3)));
+  lapply (le_mtri ????? H7 H8);
+  lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? Hletin);
+  cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))); [2:
+    apply (Eq≈  (0 + δ(an n3) (xn n3)) ? (zero_neutral ??));
+    apply (Eq≈  (δ(an n3) (xn n3) + 0) ? (plus_comm ???));
+    apply (Eq≈  (δ(an n3) (xn n3) +  (-δ(xn n3) (bn n3) +  δ(xn n3) (bn n3))) ? (opp_inverse ??));
+    apply (Eq≈  (δ(an n3) (xn n3) +  (δ(xn n3) (bn n3) + -δ(xn n3) (bn n3))) ? (plus_comm ?? (δ(xn n3) (bn n3))));
+    apply (Eq≈  ? ? (eq_sym ??? (plus_assoc ????))); assumption;] clear Hletin1;
+  apply (le_rewl ???  ( δ(an n3) (xn n3)+ δ(an n3) x));[
+    apply feq_plusr; apply msymmetric;]
+  apply (le_rewl ???  (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x));[
+    apply feq_plusr; assumption;]
+  clear Hcut Hletin Dym Dxm H8 H7 H6 H5 H4 H3;
+  apply (le_rewl ??? (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x));[
+    apply feq_plusr; apply plus_comm;]
+  apply (le_rewl ??? (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????));
+  apply (le_rewl ??? ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???));
+  apply lew_opp; [apply mpositive] apply fle_plusr;
+  apply (le_rewr ???? (plus_comm ???));
+  apply (le_rewr ??? ( δ(an n3) x+ δx (bn n3)) (msymmetric ????));
+  apply mtineq;]
+split; [
+  apply (lt_le_transitive ????? (mpositive ????));
+  split; elim He; [apply  le_zero_x_to_le_opp_x_zero; assumption;]
+  cases t1; [ 
+    left; apply exc_zero_opp_x_to_exc_x_zero;
+    apply (Ex≫ ? (eq_opp_opp_x_x ??));assumption;]
+  right;  apply exc_opp_x_zero_to_exc_zero_x;
+  apply (Ex≪ ? (eq_opp_opp_x_x ??)); assumption;]
+clear Dxm Dym H7 H8 Hn3 H5 H3 n1 n2;
+apply (le_lt_transitive ???? ? (sandwich_ineq ?? He));
+apply (le_transitive ???? Hcut);
+apply (le_transitive ??  (e/3+ δ(an n3) x+ δ(an n3) x)); [
+  repeat apply fle_plusr; cases H6; assumption;]
+apply (le_transitive ??  (e/3+ e/2 + δ(an n3) x)); [
+  apply fle_plusr; apply fle_plusl; cases H4; assumption;]
+apply (le_transitive ??  (e/3+ e/2 + e/2)); [
+  apply fle_plusl; cases H4; assumption;]
+apply le_reflexive;
+qed.