proposition: Lemma expg_order x : x ^+ #[x] = 1.
proof: Proof. have: uniq (traject (mulg x) 1 #[x]). by apply/card_uniqP; rewrite size_traject -(eq_card (cycle_traject x)). case/cyclePmin: (mem_cycle x #[x]) => [] [//|i] ltix. rewrite -(subnKC ltix) addSnnS /= expgD; move: (_ - _) => j x_j1. case/andP=> /trajectP[]; exists j; first exact: leq_addl. by apply: (mulgI (x ^+ i.+1)); rewrite -iterSr iterS -iteropE -expgS mulg1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)