proposition: Lemma asympt_eq0 (x : creal) : x == 0 -> {asympt e : i / `|x i| < e}.
proof: Proof. by move/asympt_eq; apply: asymptP=> e i; rewrite subr0. 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)