proposition: Lemma classVg x A : x^-1 ^: A = (x ^: A)^-1.
proof: Proof. apply/setP=> xy; rewrite inE; apply/imsetP/imsetP=> [] [y Ay def_xy]. by rewrite def_xy conjVg invgK; exists y. by rewrite -[xy]invgK def_xy -conjVg; exists y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)