proposition: Lemma morphX n : {in D, {morph f : x / x ^+ n}}.
proof: Proof. by elim: n => [|n IHn] x Dx; rewrite ?morph1 // !expgS morphM ?(groupX, IHn). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)