proposition: Fact coef_add_poly p q i : (add_poly p q)`_i = p`_i + q`_i.
proof: Proof. rewrite unlock coef_poly; case: leqP => //. by rewrite geq_max => /andP[le_p_i le_q_i]; rewrite !nth_default ?add0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)