proposition: Lemma Cyclotomic2 : 'Phi_2 = 'X + 1.
proof: Proof. have := @prod_Cyclotomic 2%N isT; rewrite !big_cons big_nil mulr1/=. rewrite Cyclotomic1 -(@expr1n {poly int} 2%N). by rewrite subr_sqr expr1n => /mulfI->//; rewrite polyXsubC_eq0. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(char0 various)