proposition: Lemma root_root_seq (p : {poly F}) x : p != 0 -> x \in root_seq p = root p x.
proof: Proof. rewrite /root_seq; set loop := fix loop p n := if n is _.+1 then _ else _. elim: size {-2 5}p (erefl (size p))=> /= {p} [|n ihn] p /=. by move/eqP; rewrite size_poly_eq0 => /eqP->; rewrite eqxx. case: eqP=> /= [sp_neq1 sp_eqn|/negP]; last first. rewrite negbK=> /size_poly1P [c c_neq0 ->] _ _. by rewrite rootC (negPf c_neq0). case: sigW => z /= rpz p_neq0. rewrite in_cons; have [->|neq_xz] //= := altP eqP. move: rpz sp_eqn => /factor_theorem [q ->]. rewrite mulpK ?polyXsubC_eq0 // rootM root_XsubC (negPf neq_xz) orbF. have [->|q_neq0] := eqVneq q 0; first by rewrite mul0r size_poly0. rewrite size_mul ?polyXsubC_eq0 // size_XsubC addn2. by case=> /ihn /(_ q_neq0). Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)