proposition: Lemma prod_factor (p : {poly F}): p = (lead_coef p) *: \prod_(x <- linear_factor_seq p) x.
proof: Proof. by rewrite !big_map {1}[p]prod_XsubC_mu. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)