proposition: Lemma monic_prod_factor p : p \is monic -> p = \prod_(x <- linear_factor_seq p) x.
proof: Proof. by move/monicP=> H; rewrite {1}[p]prod_factor H scale1r. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)