proposition: Lemma complgC H K G : (H \in [complements to K in G]) = (K \in [complements to H in G]).
proof: Proof. rewrite !inE setIC; congr (_ && _). by apply/eqP/eqP=> defG; rewrite -(comm_group_setP _) // defG groupP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)