proposition: Lemma asympt1modP (R : numDomainType) P (a : asympt1 P) e i : 0 < e :> R -> (projT1 a e <= i)%N -> P e i.
proof: Proof. by case: a e i. 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)