proposition: Fact coef_opp_poly p i : (opp_poly p)`_i = - p`_i.
proof: Proof. rewrite unlock coef_poly /=. by case: leqP => // le_p_i; rewrite nth_default ?oppr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)