proposition: Lemma sub_root_div (p q : {poly F}) (Hq : q != 0) : p %| q -> {subset (root_seq p) <= (root_seq q)} .
proof: Proof. case: (eqVneq p 0) => [->|p0]; first by rewrite root_seq0. by case/dvdpP => x Hx y; rewrite !root_root_seq // Hx rootM orbC=> ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)