proposition: Theorem groupExp_mod : forall g n, generator g -> g^n = g^(modNat n order).
proof: Proof. intuition. eapply groupExp_eq_if. trivial. rewrite (@modNat_eq _ (modNat n order)). trivial. eapply modNat_lt. Qed.
imports: FCF.Rat FCF.StdNat