proposition: Lemma prod_XsubC_count (p : {poly F}): p = (lead_coef p) *: \prod_(x <- root_seq_uniq p) ('X - x%:P)^+ (count_mem x (root_seq p)).
proof: Proof. by rewrite {1}[p]root_seq_eq (prod_seq_count (root_seq p)). Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)