proposition: Theorem PedersenInfoTheoreticHiding : Pr[HidingCommit_G PedersenSetup PedersenCommit A1 A2] == 1/2.
proof: Proof. rewrite PedersenHiding_G0_equiv. rewrite PedersenHiding_G1_equiv. rewrite PedersenHiding_G2_equiv. rewrite PedersenHiding_G3_equiv. apply PedersenHiding_G3_half. Qed.
imports: FCF GroupTheory OTP RndNat RndGrpElem