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