proposition: Lemma eq0_modP (x : creal) (x_eq0 : x == 0) eps i : 0 < eps -> (eq_mod x_eq0 eps <= i)%N -> `|x i| < eps.
proof: Proof. by move=> eps_gt0 hi; rewrite -[X in `|X|]subr0 -[0]/(0%CR i) eq_modP. 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)