proposition: Lemma basisE (p q : {poly R}) : 0 < n -> size p <= (maxn (size p %/ n) (size q %/ n)).+1 * n.
proof: Proof. move=> Hn0; move: (leq_maxl (size p %/ n).+1 (size q %/ n).+1). by rewrite -(leq_pmul2r Hn0) maxnSS; apply/leq_trans/ltnW; rewrite ltn_ceil. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div fintype tuple) mathcomp(finfun bigop fingroup perm ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly)