proposition: Lemma root_seq_eq (p : {poly F}) : p = lead_coef p *: \prod_(x <- root_seq p) ('X - x%:P).
proof: Proof. move: {2}(root_seq p) (erefl (root_seq p))=> s. elim: s p=> [p | x s IHp p H]. rewrite /root_seq; set loop := fix loop p n := if n is _.+1 then _ else _. case H: (size p)=> [|n]. move/eqP: H; rewrite size_poly_eq0=> /eqP ->. by rewrite lead_coef0 scale0r. case: n H => [H | n H] /=; case: eqP => //. move=> _ _; rewrite big_nil. move/eqP: H => /size_poly1P [c H] ->. by rewrite lead_coefC alg_polyC. by move/negP; rewrite negbK H. rewrite H big_cons (root_seq_cons H) mulrC scalerAl. have Hfp : p = p %/ ('X - x%:P) * ('X - x%:P). apply/eqP; rewrite -dvdp_eq dvdp_XsubCl -root_root_seq. by rewrite H mem_head. move: H; rewrite /root_seq. set loop := fix loop p n := if n is _.+1 then _ else _. by apply: contraPneq => ->; rewrite size_poly0. suff -> : lead_coef p = lead_coef (p %/ ('X - x%:P)). by rewrite -IHp ?(root_seq_cons H). by rewrite {1}Hfp lead_coef_Mmonic // monicXsubC. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)