proposition: Theorem PedersenHiding_G3_equiv : Pr[PedersenHiding_G2] == Pr[PedersenHiding_G3].
proof: Proof. unfold PedersenHiding_G2, PedersenHiding_G3. do 2 (inline_first; comp_skip; comp_simp). comp_swap_l. comp_skip. comp_swap_l. comp_skip. Qed.
imports: FCF GroupTheory OTP RndNat RndGrpElem