proposition: Lemma asymptP (P1 : F -> nat -> Prop) (P2 : F -> nat -> Prop) : (forall e i, 0 < e -> P1 e i -> P2 e i) -> {asympt e : i / P1 e i} -> {asympt e : i / P2 e i}.
proof: Proof. by move=> hP; case=> m hm; exists m=> e i he me; apply: hP=> //; apply: hm. 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)