proposition: Lemma coef_poly0 (p q : {poly R}) : (p * q)`_0 = p`_0 * q`_0.
proof: Proof. by rewrite coef_mul_poly big_ord_recl big_ord0 sub0n addr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc