proposition: Lemma separable_polyXnsub1 (R : fieldType) n : n%:R != 0 :> R -> separable_poly ('X^n - 1 : {poly R}).
proof: Proof. move=> nC. have n_gt0 : 0 < n by case: n nC => //; rewrite eqxx. rewrite unlock !derivE subr0. suff ->: 'X^n - 1 = (n%:R^-1 *: 'X) * ('X^n.-1 *+ n) + (-1) :> {poly R}. rewrite coprimep_sym coprimep_addl_mul. by rewrite -scaleN1r coprimepZr ?coprimep1 // oppr_eq0 oner_eq0. rewrite -scaler_nat scalerCA scalerA mulVf //. by rewrite scale1r -exprS prednK. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)