proposition: Theorem group_OTP_exp : forall (x : nat), comp_spec eq (RndG) (r <-$ [0 .. order) ; ret (g ^ x) ^r)%group.
proof: Proof. intuition. eapply comp_spec_seq; [intuition..| | ]. eapply comp_spec_symm. eapply (comp_spec_iso (fun z => modNat (x * z) order) (fun z => modNat (z * multInverseModOrder x) order)). intuition. rewrite (Nat.mul_comm x0). rewrite <- modNat_mult_eq. rewrite Nat.mul_assoc. rewrite Nat.mul_comm. rewrite modNat_mult_eq. rewrite multInverseCorrect. rewrite Nat.mul_1_r. eapply modNat_eq. eapply RndNat_support_lt. trivial. intuition. rewrite Nat.mul_comm. rewrite <- modNat_mult_eq. rewrite Nat.mul_assoc. rewrite Nat.mul_comm. rewrite modNat_mult_eq. rewrite (Nat.mul_comm _ x). rewrite multInverseCorrect. rewrite Nat.mul_1_r. eapply modNat_eq. eapply RndNat_support_lt. trivial. intuition. eapply in_getSupport_RndNat. eapply modNat_lt. intuition. eapply eq_impl_comp_spec. eapply well_formed_RndNat. intuition. eapply well_formed_RndNat. intuition. eapply RndNat_uniform. eapply modNat_lt. eapply RndNat_support_lt. trivial. intros. simpl in H2. subst. eapply comp_spec_ret. rewrite <- groupExp_mod. symmetry. apply groupExp_mult. eapply H. Qed.
imports: FCF GroupTheory OTP RndNat RndGrpElem