proposition: Lemma root_seq_cons (p : {poly F}) x s : root_seq p = x :: s -> s = root_seq (p %/ ('X - x%:P)).
proof: Proof. rewrite /root_seq; set loop := fix loop p n := if n is _.+1 then _ else _. case H: (size p)=> [|n] //=; case: eqP=> // Hp. move/eqP; rewrite eqseq_cons; case/andP=> /eqP {1}<- /eqP <-. suff ->: n = size (p %/ ('X - x%:P))=> //. by rewrite size_divp ?polyXsubC_eq0 // size_XsubC subn1 H. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)