proposition: Lemma lead_coef_XnsubC {R : ringType} n (c : R) : (0 < n)%N -> lead_coef ('X^n - c%:P) = 1.
proof: Proof. move=> gt0_n; rewrite lead_coefDl ?lead_coefXn //. by rewrite size_opp size_polyC size_polyXn ltnS (leq_trans (leq_b1 _)). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)