proposition: Theorem no_coherent_Frobenius_partition : G0 != 1%G.
proof: Proof. have [i] := coherent_Frobenius_bound; apply: contraTneq => ->. have [] := e_bounds i; set e := e_ i; set h := h_ i => e_gt1 le_e_h2. rewrite cards1 subrr mul0r lt_geF // pmulr_rgt0 ?subr_gt0 // ltr_wpDl //. rewrite ?(mulr_ge0, invr_ge0) ?ler0n // addrAC subr_ge0. by rewrite -[_ - 1](@divfK _ 2%:R) ?pnatr_eq0 // mulrC ler_wpM2r ?ler0n. by rewrite -natrD addnC ?(pmulr_rgt0, invr_gt0) ?ltr0n. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup commutator nilpotent frobenius) mathcomp(matrix mxalgebra mxrepresentation) odd_order(BGsection3) mathcomp(vector ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection4 PFsection5 PFsection6)