proposition: Lemma groupExp_eq_h : forall g c1 v, generator g -> v < order -> g^(c1 * order + v) = g^v.
proof: Proof. induction c1; intuition; simpl in *. rewrite <- Nat.add_assoc. rewrite (groupExp_plus order). rewrite groupOrder; trivial. rewrite groupIdent; trivial. rewrite left_identity. rewrite IHc1; trivial. Qed.
imports: FCF.Rat FCF.StdNat