proposition: Lemma consttM pi x y : commute x y -> (x * y).`_pi = x.`_pi * y.`_pi.
proof: Proof. move=> cxy; pose m := #|<<[set x; y]>>|; have m_gt0: 0 < m := cardG_gt0 _. pose k := chinese m`_pi m`_pi^' 1 0. suffices kXpi z: z \in <<[set x; y]>> -> z.`_pi = z ^+ k. by rewrite !kXpi ?expgMn // ?groupM ?mem_gen // !inE eqxx ?orbT. move=> xyz; have{xyz} zm: #[z] %| m by rewrite cardSg ?cycle_subG. apply/eqP; rewrite eq_expg_mod_order -{3 4}[#[z]](partnC pi) //. rewrite chinese_remainder ?chinese_modl ?chinese_modr ?coprime_partC //. rewrite -!(modn_dvdm k (partn_dvd _ m_gt0 zm)). rewrite chinese_modl ?chinese_modr ?coprime_partC //. by rewrite !modn_dvdm ?partn_dvd ?eqxx. 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)