proposition: Lemma morphJ : {in D &, {morph f : x y / x ^ y}}.
proof: Proof. by move=> * /=; rewrite !morphM ?morphV // ?groupM ?groupV. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)