forall (y : Approximation A) ly, IsLimit y ly -> forall u e d, close e u (y d) -> close (e+d) u ly. Proof. intros y ly E1 u e d xi. apply (merely_destruct ((fst (rounded _ _ _) xi))). intros [d0 [d' [He E2]]]. pose proof (triangular _ _ _ _ _ E2 (E1 d' _)) as E3. assert (Hrw : e + d = d0 + (d' + d));[|rewrite Hrw;trivial]. rewrite He. symmetry. apply Qpos_plus_assoc. Qed.
Require Import Import NatPair.Instances. Import Quoting.Instances.