proposition: Lemma size_XnsubC {R : ringType} n (c : R) : (0 < n)%N -> size ('X^n - c%:P) = n.+1.
proof: Proof. move=> gt0_n; rewrite size_addl ?size_polyXn //. by rewrite size_opp size_polyC; case: (c =P 0). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)