proposition: Lemma test_bij' (i j : pid) (m : chMap pid (chProd public choiceTranscript1)) : (i != j)%N → ∃ (f : secret → secret), ∀ (x : secret), bijective f /\ (∀ zk, compute_key (setm m j (fto (g ^+ otf x), zk)) i = g ^+ (otf (f x))).
proof: Proof. simpl. intros ne. have [f H] := test_bij i j m ne. simpl in H. exists (fun (x : secret) => fto (f (otf x))). intro x. destruct (H (otf x)) as [f_bij H'] ; clear H. split. - exists (fun z => fto ((finv f) (otf z))). + apply bij_inj in f_bij. intro z. rewrite otf_fto. apply finv_f in f_bij. rewrite f_bij fto_otf. reflexivity. + apply bij_inj in f_bij. intro z. rewrite otf_fto. apply f_finv in f_bij. rewrite f_bij fto_otf. reflexivity. - intro zk. specialize (H' zk). rewrite otf_fto. apply H'. 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)