proposition: Lemma monic_linear_factor_seq p : forall q, q \in linear_factor_seq p -> q \is monic.
proof: Proof. move=> q Hq; rewrite -(nth_index 0 Hq) (nth_map (0,0%N)). apply: monic_exp; first by apply: monicXsubC. by rewrite -index_mem size_map in Hq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)