proposition: Fact coef_mul_poly p q i : (mul_poly p q)`_i = \sum_(j < i.+1) p`_j * q`_(i - j)%N.
proof: Proof. rewrite unlock coef_poly -subn1 ltn_subRL add1n; case: leqP => // le_pq_i1. rewrite big1 // => j _; have [lq_q_ij | gt_q_ij] := leqP (size q) (i - j). by rewrite [q`__]nth_default ?mulr0. rewrite nth_default ?mul0r // -(leq_add2r (size q)) (leq_trans le_pq_i1) //. by rewrite -leq_subLR -subnSK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)