proposition: Lemma irredp_XaddC (F : fieldType) (x : F) : irreducible_poly ('X + x%:P).
proof: Proof. by rewrite -[x]opprK rmorphN; apply: irredp_XsubC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)