proposition: Lemma rootsE (R : rcfType) a b (p : {poly R}) : p != 0 -> roots p a b = [seq x <- rootsR p | a < x < b].
proof: Proof. move=> p_neq0; symmetry; apply: roots_uniq => //. by move=> i; rewrite !inE/= mem_filter mem_rootsR. by rewrite (sorted_filter lt_trans)// sorted_roots. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf polyorder) Abel(various)