proposition: Lemma root_seq_nil (p : {poly F}) : (size p <= 1)%N = ((root_seq p) == [::]).
proof: Proof. by rewrite -subn_eq0 subn1 -size_root_seq size_eq0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_real_closed) CoqEAL(ssrcomplements)