proposition: Lemma morph_constt pi x : x \in D -> f x.`_pi = (f x).`_pi.
proof: Proof. move=> Dx; rewrite -{2}(consttC pi x) morphM ?groupX //. rewrite consttM; last by rewrite !morphX //; apply: commuteX2. have: pi.-elt (f x.`_pi) by rewrite morph_p_elt ?groupX ?p_elt_constt //. have: pi^'.-elt (f x.`_pi^') by rewrite morph_p_elt ?groupX ?p_elt_constt //. by move/constt1P->; move/constt_p_elt->; rewrite mulg1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)