proposition: Lemma lead_coef_XsubC {R : ringType} (c : R) : lead_coef ('X - c%:P) = 1.
proof: Proof. by apply: (@lead_coef_XnsubC _ 1%N). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)