proposition: Lemma splitsP B A : reflect (exists H, H \in [complements to A in B]) [splits B, over A].
proof: Proof. exact: set0Pn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)