proposition: Lemma poly_XnsubC_over {R : ringType} n c (S : subringClosed R) : c \in S -> 'X^n - c%:P \is a polyOver S.
proof: Proof. by move=> cS; rewrite rpredB ?rpredX ?polyOverX ?polyOverC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)