proposition: Lemma lead_coef_comp p q : size q > 1 -> lead_coef (p \Po q) = (lead_coef p) * lead_coef q ^+ (size p).-1.
proof: Proof. move=> q_gt1; rewrite !lead_coefE coef_comp_poly size_comp_poly. have [->|nz_p] := eqVneq p 0; first by rewrite size_poly0 big_ord0 coef0 mul0r. rewrite polySpred //= big_ord_recr /= big1 ?add0r => [|i _]. by rewrite -!lead_coefE -lead_coef_exp !lead_coefE size_exp mulnC. rewrite [X in _ * X]nth_default ?mulr0 ?(leq_trans (size_exp_leq _ _)) //. by rewrite mulnC ltn_mul2r -subn1 subn_gt0 q_gt1 /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)