proposition: Lemma mem_rootsR (R : rcfType) (p : {poly R}) : p != 0 -> rootsR p =i root p.
proof: Proof. by move=> x pneq0; rewrite -roots_on_rootsR. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf polyorder) Abel(various)