include "sandwich.ma".
-include "metric_lattice.ma".
-
(* 3.17 *)
lemma tends_uniq:
- ∀R.∀ml:mlattice R.∀xn:sequence ml.
- ∀x,y:apart_of_metric_space ? ml.
- (* BUG: it inserts a compesoed coercion instead of an hand made one,
- what to do? prefer the human made one or allow to kill a coercion?
- *)
- xn ⇝ x → xn ⇝ y → x ≈ y.
+ ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x,y:ml.
+ xn ⇝ x → xn ⇝ y → δ x y ≈ 0.
intros (R ml xn x y H1 H2); unfold tends0 in H1 H2; unfold d2s in H1 H2;
-intro Axy; lapply (ap2delta R ml x y Axy) as ge0;
+intro Axy; lapply (ap_le_to_lt ??? (ap_symmetric ??? Axy) (mpositive ? ml ??)) as ge0;
cases (H1 (δ x y/1) (divide_preserves_lt ??? ge0)) (n1 Hn1); clear H1;
cases (H2 (δ x y/1) (divide_preserves_lt ??? ge0)) (n2 Hn2); clear H2;
letin N ≝ (S (n2 + n1));