proposition: Lemma eq_modP (x y : creal) (eq_xy : x == y) eps i : 0 < eps -> (eq_mod eq_xy eps <= i)%N -> `|x i - y i| < eps.
proof: Proof. by move=> eps_gt0; rewrite /eq_mod; case: (asympt_eq _)=> /= m hm /hm; apply. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)