proposition: Lemma invSg A B : (A^-1 \subset B^-1) = (A \subset B).
proof: Proof. by rewrite !(sameP setIidPl eqP) -invIg (inj_eq invg_inj). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)