proposition: Lemma morphpreV R : f @*^-1 R^-1 = (f @*^-1 R)^-1.
proof: Proof. apply/setP=> x; rewrite !inE groupV; case Dx: (x \in D) => //=. by rewrite morphV. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)