proposition: Theorem groupExp_eq : forall g x y, generator g -> g^x = g^y -> modNat x order = modNat y order.
proof: Proof. intuition. erewrite <- groupLog_correct; eauto. erewrite <- (groupLog_correct _ y); eauto. f_equal. f_equal. trivial. Qed.
imports: FCF.Rat FCF.StdNat