proposition: Lemma le_modP (x y : creal) (le_xy : (x <= y)%CR) eps i : 0 < eps -> (le_mod le_xy eps <= i)%N -> x i < y i + eps.
proof: Proof. by move=> eps_gt0; rewrite /le_mod; case: (asympt_le _)=> /= 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)