proposition: Lemma solvable_AltF : 4 < #|T| -> solvable 'Alt_T = false.
proof: Proof. move=> card_T; apply/negP => Alt_solvable. have/simple_Alt5 Alt_simple := card_T. have := simple_sol_prime Alt_solvable Alt_simple. have lt_T n : n <= 4 -> n < #|T| by move/leq_ltn_trans; apply. have -> : #|('Alt_T)%G| = #|T|`! %/ 2 by rewrite -card_Alt ?mulKn ?lt_T. move/even_prime => [/eqP|]; apply/negP. rewrite neq_ltn leq_divRL // mulnC -[2 * 3]/(3`!). by apply/orP; right; apply/ltnW/ltn_fact/lt_T. by rewrite -dvdn2 dvdn_divRL dvdn_fact //=; apply/ltnW/lt_T. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)