lim_same_distance@{} : forall (x y : Approximation A) e, (forall d n, close (e+d) (x n) (y n)) -> forall d, close (e+d) (lim x) (lim y). Proof. intros x y e E d. apply equiv_lim_lim with (d/3) (d/3) (e + d/3);[|apply E]. path_via (e + 3 / 3 * d). - rewrite pos_recip_r,Qpos_mult_1_l;trivial. - apply pos_eq;ring_tac.ring_with_nat. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.