proposition: Lemma morphV : {in D, {morph f : x / x^-1}}.
proof: Proof. move=> x Dx; apply: (mulgI (f x)). by rewrite -morphM ?groupV // !mulgV morph1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)