proposition: Lemma sub_conjg A B x : (A :^ x \subset B) = (A \subset B :^ x^-1).
proof: Proof. by rewrite -(conjSg A _ x) conjsgKV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)