proposition: Lemma expg_mod_order x i : x ^+ (i %% #[x]) = x ^+ i.
proof: Proof. by rewrite expg_mod // expg_order. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)