proposition: Lemma vote_hiding_bij (c : secret) (v : bool): fto (otf (fto (g ^+ c)) * g ^+ v) = fto (otf (fto (g ^+ (if v then fto (Zp_add (otf c) Zp1) else fto (Zp_add (otf c) (Zp_opp Zp1))))) * g ^+ (~~ v)).
proof: Proof. f_equal. rewrite !otf_fto. rewrite -!expgD. have h' : ∀ (x : Secret), nat_of_ord x = (nat_of_ord (fto x)). { unfold fto. intros k. rewrite enum_rank_ord. done. } case v. ++ apply /eqP. rewrite eq_expg_mod_order. rewrite addn0. have h : ∀ (x : secret), (((nat_of_ord x) + 1) %% q'.+2)%N = (nat_of_ord (Zp_add (otf x) Zp1)). { intro k. unfold Zp_add. simpl. rewrite -Hord. apply /eqP. rewrite eq_sym. apply /eqP. rewrite -> Zp_cast at 2. 2: apply (prime_gt1 prime_order). rewrite -> Zp_cast at 1. 2: apply (prime_gt1 prime_order). rewrite modnDmr. rewrite Fp_cast. 2: apply prime_order. reflexivity. } rewrite -h'. rewrite -h. rewrite -modn_mod. rewrite Fp_cast. 2: apply prime_order. 1: apply eq_refl. ++ apply /eqP. rewrite eq_expg_mod_order. rewrite addn0. unfold Zp_add, Zp_opp, Zp1. simpl. repeat rewrite -> Zp_cast at 12. 2-4: apply (prime_gt1 prime_order). rewrite -!Hord. have -> : (#[g] - 1 %% #[g])%N = #[g].-1. { rewrite modn_small. 2: apply (prime_gt1 prime_order). by rewrite -subn1. } rewrite modn_small. 2:{ destruct c as [c Hc]. move: Hc. simpl. unfold DDH.i_space, DDHParams.Space, Secret. rewrite card_ord. rewrite Zp_cast. 2: apply (prime_gt1 prime_order). done. } have -> : (#[g].-1 %% #[g])%N = #[g].-1. { rewrite modn_small. 1: reflexivity. apply ltnSE. rewrite -subn1 -2!addn1. rewrite subnK. 2: apply (prime_gt0 prime_order). rewrite addn1. apply ltnSn. } rewrite -h'. simpl. rewrite -> Zp_cast at 9. 2: apply (prime_gt1 prime_order). rewrite modnDml. rewrite -subn1. rewrite -addnA. rewrite subnK. 2: apply (prime_gt0 prime_order). rewrite -modnDmr. rewrite modnn. rewrite addn0. rewrite modn_small. 1: apply eq_refl. destruct c as [h Hc]. move: Hc. unfold DDH.i_space, DDHParams.Space, Secret. simpl. rewrite card_ord. rewrite Zp_cast. 2: apply (prime_gt1 prime_order). done. 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) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_composition Package Prelude SigmaProtocol Schnorr DDH) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)