proposition: Lemma monic_comp_poly (p q : {poly R}) : p \is monic -> q \is monic -> q != 1 -> p \Po q \is monic.
proof: Proof. move=> pM qM qD1. have := size_comp_poly_leq p q. suff cp0q : (p \Po q)`_((size p).-1 * (size q).-1) == 1. rewrite qualifE /= /lead_coef leq_eqVlt => /orP[/eqP-> //|]; last first. rewrite ltnS => sLp; move: cp0q. by rewrite nth_default // eq_sym oner_eq0. rewrite comp_polyE coef_sum. have := (pM); rewrite monicE /lead_coef. have : (0 < size p)%nat. by have := monic_neq0 pM; rewrite -size_poly_eq0; case: size. case: size => //= k _ pkE. rewrite big_ord_recr /= (eqP pkE) scale1r big1 ?add0r. have := monic_exp k qM. by rewrite qualifE /= /lead_coef size_exp_monic //= mulnC. move=> i _; rewrite coefZ [_`_(k * _)]nth_default ?mulr0 //. rewrite size_exp_monic // mulnC. suff : (1 < size q)%nat. by case: size => // [] [|v] //_ ; rewrite ltn_mul2r ltn_ord. case E : size => [|[|v]] //. have /eqP := E; rewrite size_poly_eq0 => /eqP qE0. by move: qM; rewrite qualifE /= qE0 lead_coefC eq_sym oner_eq0. have /eqP/size_poly1P[c cD0 qE] := E. by case/eqP: qD1; move: qM; rewrite qE qualifE /= lead_coefC => /eqP->. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)