(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/sandwich/".
+
include "nat/plus.ma".
include "nat/orders.ma".
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:
+let ugo ≝ excess_OF_lattice1 in
∀R.∀ml:mlattice R.∀an,bn,xn:sequence ml.∀x:ml.
- (∀n. (an n ≤ xn n) ∧ (xn n ≤ bn n)) →
+ (∀n. (le (excess_OF_lattice1 ml) (xn n) (an n)) ∧
+ (le (excess_OF_lattice1 ?) (bn n) (xn n))) → True.
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);
(* the main inequality *)
cut (δ (xn n3) x ≤ δ (bn n3) x + δ (an n3) x + δ (an n3) x) as main_ineq; [2:
apply (le_transitive ???? (mtineq ???? (an n3)));
- lapply (le_mtri ????? H7 H8) as H9; clear H7 H8;
- lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9;
cut ( δ(an n3) (bn n3)+- δ(xn n3) (bn n3)≈( δ(an n3) (xn n3))) as H11; [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 H10;
- apply (le_rewl ??? ( δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3)));
- apply (le_rewl ??? (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11);
+ lapply (le_mtri ?? ??? (ge_to_le ??? H7) (ge_to_le ??? H8)) as H9; clear H7 H8;
+ lapply (feq_plusr ? (- δ(xn n3) (bn n3)) ?? H9) as H10; clear H9;
+ 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;]
+ apply (Le≪ (δ(an n3) (xn n3)+ δ(an n3) x) (msymmetric ??(an n3)(xn n3)));
+ apply (Le≪ (δ(an n3) (bn n3)+- δ(xn n3) (bn n3)+ δ(an n3) x) H11);
apply (Le≪ (- δ(xn n3) (bn n3)+ δ(an n3) (bn n3)+δ(an n3) x) (plus_comm ??(δ(an n3) (bn n3))));
apply (Le≪ (- δ(xn n3) (bn n3)+ (δ(an n3) (bn n3)+δ(an n3) x)) (plus_assoc ????));
apply (Le≪ ((δ(an n3) (bn n3)+δ(an n3) x)+- δ(xn n3) (bn n3)) (plus_comm ???));