proposition: Lemma separable_Xn_sub_1 (R : idomainType) n : n%:R != 0 :> R -> @separable_poly R ('X^n - 1).
proof: Proof. case: n => [/eqP// | n nz_n]; rewrite unlock linearB /= derivC subr0. rewrite derivXn -scaler_nat coprimepZr //= exprS -scaleN1r coprimep_sym. by rewrite coprimep_addl_mul coprimepZr ?coprimep1 // (signr_eq0 _ 1). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly finset fingroup finalg zmodp cyclic) mathcomp(ssrnum ssrint archimedean polydiv intdiv mxpoly) mathcomp(rat vector falgebra fieldext separable galois algC)