proposition: Lemma rank3_SCN3 : exists B, B \in 'SCN_3(R).
proof: Proof. by apply/set0Pn; rewrite -(rank2_SCN3_empty pR oddR) leqNgt (rank_pgroup pR) rR. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finset prime fingroup morphism perm automorphism action) mathcomp(quotient cyclic gfunctor pgroup gproduct center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection4)