proposition: Theorem groupExp_eq_if : forall g x y, generator g -> modNat x order = modNat y order -> g^x = g^y.
proof: Proof. intuition. destruct (modNat_correct x order). destruct (modNat_correct y order). rewrite H1. rewrite H2. rewrite H0. repeat rewrite groupExp_eq_h; eauto using modNat_lt. Qed.
imports: FCF.Rat FCF.StdNat