proposition: Lemma comp_poly_eq0 p q : size q > 1 -> (p \Po q == 0) = (p == 0).
proof: Proof. move=> sq_gt1; rewrite -!lead_coef_eq0 lead_coef_comp //. rewrite mulf_eq0 expf_eq0 !lead_coef_eq0 -[q == 0]size_poly_leq0. by rewrite [_ <= 0]leqNgt (leq_ltn_trans _ sq_gt1) ?andbF ?orbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)