forall u (y : Approximation A) e d, close e u (y d) -> close (e+d) u (lim y). Proof. intros u y;apply equiv_through_approx0. apply cauchy_complete. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.