proposition: Lemma complP H A B : reflect (A :&: H = 1 /\ A * H = B) (H \in [complements to A in B]).
proof: Proof. by apply: (iffP setIdP); case; split; apply/eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)