proposition: Lemma equiv_through_approx0 : forall (y : Approximation A) ly, IsLimit y ly -> forall u e d, close e u (y d) -> close (e+d) u ly.
proof: 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.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.rationals HoTT.Classes.interfaces.orders HoTT.Classes.implementations.peano_naturals HoTT.Classes.implementations.natpair_integers HoTT.Classes.theory.groups HoTT.Classes.theory.integers HoTT.Classes.theory.dec_fields HoTT.Classes.orders.dec_fields HoTT.Classes.orders.sum HoTT.Classes.theory.rationals HoTT.Classes.orders.lattices HoTT.Classes.implementations.assume_rationals HoTT.Classes.tactics.ring_quote HoTT.Classes.tactics.ring_tac