proposition: Lemma equiv_lim_lim (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: 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.
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