proposition: Lemma monic_XsubC {R : ringType} (c : R) : 'X - c%:P \is monic.
proof: Proof. by rewrite monicE lead_coef_XsubC. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)