proposition: Lemma mul_lead_coef p q : lead_coef p * lead_coef q = (p * q)`_(size p + size q).-2.
proof: Proof. pose dp := (size p).-1; pose dq := (size q).-1. have [-> | nz_p] := eqVneq p 0; first by rewrite lead_coef0 !mul0r coef0. have [-> | nz_q] := eqVneq q 0; first by rewrite lead_coef0 !mulr0 coef0. have ->: (size p + size q).-2 = (dp + dq)%N. by do 2!rewrite polySpred // addSn addnC. have lt_p_pq: dp < (dp + dq).+1 by rewrite ltnS leq_addr. rewrite coefM (bigD1 (Ordinal lt_p_pq)) ?big1 ?simp ?addKn //= => i. rewrite -val_eqE neq_ltn /= => /orP[lt_i_p | gt_i_p]; last first. by rewrite nth_default ?mul0r //; rewrite -polySpred in gt_i_p. rewrite [q`__]nth_default ?mulr0 //= -subSS -{1}addnS -polySpred //. by rewrite addnC -addnBA ?leq_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)