(x y : Approximation A) (e d n e' : Q+) : e = d + n + e' -> close e' (x d) (y n) -> close e (lim x) (lim y). Proof. intros He xi. rewrite He. assert (Hrw : d + n + e' = e' + d + n) by (apply pos_eq;ring_tac.ring_with_nat); rewrite Hrw;clear Hrw. apply equiv_through_approx. symmetry. apply equiv_through_approx. symmetry;trivial. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.