proposition: Lemma bijective_expgn : bijective (λ (a : 'Z_q), g ^+ a).
proof: Proof. unshelve eexists (λ x, (proj1_sig (@cyclePmin gT g x _) %% q)%:R). - rewrite -g_gen. unfold ζ. apply in_setT. - simpl. intros a. match goal with | |- context [ @cyclePmin _ _ _ ?hh ] => set (h := hh) end. clearbody h. simpl in h. destruct cyclePmin as [n hn e]. simpl. move: e => /eqP e. rewrite eq_expg_mod_order in e. move: e => /eqP e. rewrite -e. rewrite modn_small. 2:{ fold q. eapply leq_trans. 1: eapply ltn_ord. rewrite Zp_cast. 2: apply order_gt1. auto. } apply natr_Zp. - simpl. intro x. match goal with | |- context [ @cyclePmin _ _ _ ?hh ] => set (h := hh) end. clearbody h. simpl in h. destruct cyclePmin as [n hn e]. simpl. subst. rewrite modn_small. 2: auto. f_equal. rewrite val_Zp_nat. 2: apply order_gt1. apply modn_small. auto. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum fingroup.fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude AsymScheme) Coq(Utf8) extructures(ord fset fmap) Equations(Equations)