proposition: Lemma prod_XsubC_mu (p : {poly F}): p = (lead_coef p) *: \prod_(x <- root_seq_uniq p) ('X - x%:P)^+(\mu_x p).
proof: Proof. rewrite {1}[p]prod_XsubC_count. by congr GRing.scale; apply: eq_bigr => i _; rewrite count_root_seq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)