proposition: Lemma solvable_SymF : 4 < #|T| -> solvable 'Sym_T = false.
proof: Proof. by rewrite (series_sol (Alt_normal T)) => /solvable_AltF->. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)