diff --git a/VerifiedCommitments/BindingEncryption.lean b/VerifiedCommitments/BindingEncryption.lean
new file mode 100644
index 0000000..5280df4
--- /dev/null
+++ b/VerifiedCommitments/BindingEncryption.lean
@@ -0,0 +1,32 @@
+import VerifiedCommitments.elgamal
+
+variable {X Y L R : Type}
+
+structure BindingEncryptionScheme (X Y L R : Type) where
+  gen : PMF (L × L)
+  enc : L → X → R → Y
+  dec : L → Y → X
+
+
+def correctness (scheme : BindingEncryptionScheme X Y L R) : Prop :=
+  ∀ (m : X) (r : R) (sk pk : L), scheme.dec sk (scheme.enc pk m r) = m
+
+variable {G : Type} [params : Elgamal.ElgamalParameters G]
+instance : DecidableEq G := params.decidable_G
+instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩
+
+noncomputable def setup : PMF (ZMod params.q × G) := --Elgamal.keygen
+  PMF.uniformOfFintype (ZMod params.q) |>.bind (fun x => pure (x, params.g^x.val))
+
+noncomputable def commit (h m : G) : PMF (G × ZMod params.q) := --(Elgamal.encrypt h m).map (fun (_, b) => b)
+  PMF.uniformOfFintype (ZMod params.q) |>.bind (fun r => pure (h^r.val * m, r))
+
+def verify (h m c : G) (o : ZMod params.q) : ZMod 2 := --if c = Elgamal.encrypt h m
+  if c = h^o.val * m then 1 else 0
+
+noncomputable def scheme : BindingEncryptionScheme G G G (ZMod params.q) :=
+  {
+    gen := setup,
+    enc := commit,
+    dec := verify
+  }
diff --git a/VerifiedCommitments/CommitmentScheme.lean b/VerifiedCommitments/CommitmentScheme.lean
index 6a0ac0e..046ae87 100644
--- a/VerifiedCommitments/CommitmentScheme.lean
+++ b/VerifiedCommitments/CommitmentScheme.lean
@@ -1,6 +1,7 @@
 import Mathlib.Probability.ProbabilityMassFunction.Basic
 import Mathlib.Probability.ProbabilityMassFunction.Monad
 import Mathlib.Probability.ProbabilityMassFunction.Constructions
+import Mathlib.Probability.Distributions.Uniform
 import Mathlib.Data.ZMod.Defs
 
 structure CommitmentScheme (M C O K : Type) where
@@ -15,14 +16,17 @@ structure BindingGuess (M C O : Type) where
   o : O
   o': O
 
+structure TwoStageAdversary (K M C : Type) where
+  State : Type
+  stage1 : K → PMF ((M × M) × State)
+  stage2 : C → State → PMF (ZMod 2)
+
 namespace Commitment
 
 noncomputable section
 variable {M C O K : Type}
 variable (scheme : CommitmentScheme M C O K)
 
-variable (h : K)
-
 def correctness (scheme : CommitmentScheme M C O K) : Prop :=
   ∀ (h : K) (m : M),
   PMF.bind (scheme.commit h m) (fun (commit, opening_val) => pure $ scheme.verify h m commit opening_val) = pure 1
@@ -42,9 +46,9 @@ def perfect_binding (scheme : CommitmentScheme M C O K) : Prop :=
 def comp_binding_game (scheme : CommitmentScheme M C O K)
   (A' : K → PMF (BindingGuess M C O)) : PMF $ ZMod 2 :=
   open scoped Classical in
-  PMF.bind scheme.setup (fun h =>
-    PMF.bind (A' h.1) (fun guess =>
-      if scheme.verify h.1 guess.m guess.c guess.o = 1 ∧ scheme.verify h.1 guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m' then pure 1 else pure 0 ))
+  PMF.bind scheme.setup (fun (h, _) =>
+    PMF.bind (A' h) (fun guess =>
+      if scheme.verify h guess.m guess.c guess.o = 1 ∧ scheme.verify h guess.m' guess.c guess.o' = 1 ∧ guess.m ≠ guess.m' then pure 1 else pure 0 ))
 
 def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
   ∀ (A' : K → PMF (BindingGuess M C O )), comp_binding_game scheme A' 1 ≤ ε
@@ -52,22 +56,23 @@ def computational_binding [DecidableEq M] (scheme : CommitmentScheme M C O K) (
 
 -- Perfect hiding
 def do_commit (scheme: CommitmentScheme M C O K) (m : M) : PMF C :=
-PMF.bind scheme.setup (fun h =>
-  PMF.bind (scheme.commit h.1 m) (fun commit => pure commit.1))
+PMF.bind scheme.setup (fun (h, _) =>
+  PMF.bind (scheme.commit h m) (fun (c, _) => pure c))
 
 def perfect_hiding (scheme: CommitmentScheme M C O K) : Prop :=
   ∀ (m m' : M) (c : C), (do_commit scheme m) c = (do_commit scheme m') c
 
 -- Computational hiding game
-def comp_hiding_game (scheme : CommitmentScheme M C O K)
-  (A : K → C → PMF (ZMod 2)) (m : M) : PMF (ZMod 2) :=
-  PMF.bind scheme.setup (fun h =>
-    PMF.bind (scheme.commit h.1 m) (fun commit => A h.1 commit.1))
+def comp_hiding_game (scheme : CommitmentScheme M C O K) (A : TwoStageAdversary K M C) :=
+  PMF.bind scheme.setup (fun (h, _) =>
+    PMF.bind (A.stage1 h) (fun ((m₀, m₁), state) =>
+      PMF.bind (PMF.uniformOfFintype (ZMod 2)) (fun b =>
+        PMF.bind (scheme.commit h (if b = 0 then m₀ else m₁)) (fun (c, _) =>
+          PMF.bind (A.stage2 c state) (fun b' =>
+            pure (1 + b + b'))))))
 
 def computational_hiding (scheme : CommitmentScheme M C O K) (ε : ENNReal) : Prop :=
-  ∀ (A : K → C → PMF (ZMod 2)) (m₀ m₁ : M),
-  comp_hiding_game scheme A m₀ 1 - comp_hiding_game scheme A m₁ 1 ≤ ε ||
-  comp_hiding_game scheme A m₁ 1 - comp_hiding_game scheme A m₀ 1 ≤ ε
+  ∀ (A : TwoStageAdversary K M C), comp_hiding_game scheme A 1 - 1/2 ≤ ε
 
 end
 
diff --git a/VerifiedCommitments/ElgamalCommitments.lean b/VerifiedCommitments/ElgamalCommitments.lean
new file mode 100644
index 0000000..24fb2d8
--- /dev/null
+++ b/VerifiedCommitments/ElgamalCommitments.lean
@@ -0,0 +1,393 @@
+-- From cryptolib licensed under Apache 2.0
+-- https://github.com/joeylupo/cryptolib
+
+/-
+ -----------------------------------------------------------
+  Correctness and semantic security of ElGamal public-key
+  encryption scheme
+ -----------------------------------------------------------
+-/
+
+import Mathlib
+import VerifiedCommitments.cryptolib
+import VerifiedCommitments.CommitmentScheme
+
+namespace DDH
+
+variable (G : Type) [Fintype G] [Group G]
+          (g : G) (g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g)
+          (q : ℕ) [NeZero q] [Fact (0 < q)] (G_card_q : Fintype.card G = q)
+          (D : G → G → G → PMF (ZMod 2))
+
+include g_gen_G G_card_q
+
+instance : Fintype (ZMod q) := ZMod.fintype q
+
+noncomputable def Game0 : PMF (ZMod 2) :=
+do
+  let x ← PMF.uniformOfFintype (ZMod q)
+  let y ← PMF.uniformOfFintype (ZMod q)
+  let b ← D (g^x.val) (g^y.val) (g^(x.val * y.val))
+  pure b
+
+noncomputable def Game1 : PMF (ZMod 2) :=
+do
+  let x ← PMF.uniformOfFintype (ZMod q)
+  let y ← PMF.uniformOfFintype (ZMod q)
+  let z ← PMF.uniformOfFintype (ZMod q)
+  let b ← D (g^x.val) (g^y.val) (g^z.val)
+  pure b
+
+-- DDH0(D) is the event that D outputs 1 upon receiving (g^x, g^y, g^(xy))
+-- local notation `Pr[DDH0(D)]` := (DDH0 G g g_gen_G q G_card_q D 1 : ℝ)
+
+-- DDH1(D) is the event that D outputs 1 upon receiving (g^x, g^y, g^z)
+-- local notation `Pr[DDH1(D)]` := (DDH1 G g g_gen_G q G_card_q D 1 : ℝ)
+
+def Assumption (ε : ENNReal) : Prop := (Game0 G g q D 1) - (Game1 G g q D 1) ≤ ε
+
+end DDH
+
+namespace Elgamal
+
+class ElgamalParameters (G : Type) extends
+  Fintype G, Group G, IsCyclic G where
+  [decidable_G : DecidableEq G]
+  q : ℕ
+  [neZero_q : NeZero q]
+  -- [fact (0 < params.q)]
+  prime_q : Nat.Prime q
+  g : G
+  card_eq : Fintype.card G = q
+  g_gen_G : ∀ (x : G), x ∈ Subgroup.zpowers g
+  G_card_q : Fintype.card G = q
+
+-- Make instances available
+variable {G : Type} [params : ElgamalParameters G]
+instance : DecidableEq G := params.decidable_G
+instance : Fact (Nat.Prime params.q) := ⟨params.prime_q⟩
+
+noncomputable def setup : PMF (G × ZMod params.q) := -- Need to include x to match CommitmentScheme spec
+do
+  let x ← PMF.uniformOfFintype (ZMod params.q)
+  return (params.g^x.val, x)
+
+noncomputable def commit (h m : G) : PMF ((G × G) × ZMod params.q) :=
+do
+  let r ← PMF.uniformOfFintype (ZMod params.q)
+  pure ((params.g^r.val, h^r.val * m), r)
+
+def verify (h m : G) (c : (G × G)) (o : ZMod params.q) : ZMod 2 :=
+  if c = ⟨params.g^o.val, h^o.val * m⟩ then 1 else 0
+
+noncomputable def scheme : CommitmentScheme G (G × G) (ZMod params.q) G :=
+{
+  setup := setup,
+  commit := commit,
+  verify := verify
+}
+/-
+  -----------------------------------------------------------
+  Proof of correctness of ElGamal
+  -----------------------------------------------------------
+-/
+
+theorem elgamal_commitment_correctness : Commitment.correctness (@scheme G params) := by
+  intro h m
+  show PMF.bind (scheme.commit h m) _ = _
+  simp only [scheme]
+  unfold commit verify
+  simp only [bind_pure_comp, Functor.map, PMF.bind_bind, Function.comp_apply, PMF.pure_bind, ↓reduceIte, PMF.bind_const]
+
+
+/-
+  -----------------------------------------------------------
+  Proof of semantic security of ElGamal
+  -----------------------------------------------------------
+-/
+
+noncomputable def D_from_adversary (A : TwoStageAdversary G G (G × G)) : G → G → G → PMF (ZMod 2) :=
+  fun gx gy gz => do
+    let ((m₀, m₁), state) ← A.stage1 gx
+    let b ← PMF.uniformOfFintype (ZMod 2)
+    let mb := if b = 0 then m₀ else m₁
+    let b' ← A.stage2 ⟨gy, gz * mb⟩ state
+    pure (1 + b + b')
+
+/-
+  The probability of the attacker (i.e. the composition of A1 and A2)
+  winning the semantic security game (i.e. guessing the correct bit),
+  w.r.t. ElGamal is equal to the probability of D winning the game DDH0.
+-/
+theorem ComputationalHiding_DDH0 (A : TwoStageAdversary G G (G × G)) : Commitment.comp_hiding_game scheme A =  DDH.Game0 G params.g params.q (D_from_adversary A) := by
+  simp only [Commitment.comp_hiding_game, DDH.Game0, bind, scheme, setup, commit, D_from_adversary]
+  simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))]
+  apply bind_skip'
+  intro x
+  simp [pure]
+  simp_rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod params.q))]
+  apply bind_skip'
+  intro m
+  apply bind_skip'
+  intro b
+  apply bind_skip'
+  intro y
+  rw [pow_mul params.g x.val y.val]
+
+noncomputable def Game1 (A : TwoStageAdversary G G (G × G)) : PMF (ZMod 2) :=
+do
+  let x ← PMF.uniformOfFintype (ZMod params.q)
+  let y ← PMF.uniformOfFintype (ZMod params.q)
+  let ((m₀, m₁), a_state) ← A.stage1 (params.g^x.val)
+  let b ← PMF.uniformOfFintype (ZMod 2)
+  let ζ ← (do
+    let z ← PMF.uniformOfFintype (ZMod params.q)
+    let mb ← pure (if b = 0 then m₀ else m₁)
+    pure (params.g^z.val * mb))
+  let b' ← A.stage2 ⟨(params.g^y.val), ζ⟩ a_state
+  pure (1 + b + b')
+
+noncomputable def Game2 (A : TwoStageAdversary G G (G × G)) : PMF (ZMod 2) :=
+do
+  let x ← PMF.uniformOfFintype (ZMod params.q)
+  let y ← PMF.uniformOfFintype (ZMod params.q)
+  let (_, a_state) ← A.stage1 (params.g^x.val)
+  let b ← PMF.uniformOfFintype (ZMod 2)
+  let ζ ← (do
+    let z ← PMF.uniformOfFintype (ZMod params.q)
+    pure (params.g^z.val))
+  let b' ← A.stage2 ⟨(params.g^y.val), ζ⟩ a_state
+  pure (1 + b + b')
+
+
+/-
+  The probability of the attacker (i.e. the composition of A1 and A2)
+  winning Game1 (i.e. guessing the correct bit) is equal to the
+  probability of D winning the game DDH1.
+-/
+theorem Game1_DDH1 (A : TwoStageAdversary G G (G × G)) : @Game1 G params A = DDH.Game1 G params.g params.q (D_from_adversary A):= by
+  simp only [DDH.Game1, Game1, bind, D_from_adversary]
+  simp only [PMF.bind_bind, mul_ite]
+  apply bind_skip'
+  intro x
+  apply bind_skip'
+  intro y
+  -- simp_rw [PMF.bind_bind (A.stage1 _)]
+  conv_rhs => rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod params.q))]
+  apply bind_skip'
+  intro m
+  -- simp_rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod params.q))]
+  conv_lhs => rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod 2))]
+  apply bind_skip'
+  intro z
+  -- conv_rhs => rw [PMF.bind_bind (PMF.uniformOfFintype (ZMod 2))]
+  apply bind_skip'
+  intro b
+  -- simp_rw [PMF.bind_bind]
+  -- apply bind_skip'
+  -- intro mb
+  simp [pure]
+
+lemma exp_bij : Function.Bijective (fun (z : ZMod params.q) => params.g ^ z.val) := by
+  apply (Fintype.bijective_iff_surjective_and_card _).mpr
+  simp [params.card_eq]
+  intro y
+  obtain ⟨k, hk⟩ := params.g_gen_G y
+  use (k : ZMod params.q)
+  simp only at hk ⊢
+  rw [← hk]
+  suffices params.g ^ ((k : ZMod params.q).val : ℤ) = params.g ^ k by exact_mod_cast this
+  simp only [ZMod.val_intCast, ← params.card_eq]
+  exact zpow_mod_card params.g k
+
+
+lemma exp_mb_bij (mb : G) : Function.Bijective (fun (z : ZMod params.q) => params.g ^ z.val * mb) := by
+  have h : (fun (z : ZMod params.q) => params.g ^ z.val * mb) =
+    (fun (m : G) => m * mb) ∘ (fun (z : ZMod params.q) => params.g ^ z.val) := by rfl
+  rw [h]
+  apply Function.Bijective.comp
+  · -- (λ (m : G), (m * mb)) bijective
+    refine (Fintype.bijective_iff_injective_and_card _).mpr ⟨?_, rfl⟩
+    intros x y hxy
+    exact mul_right_cancel hxy
+  · -- (λ (z : ZMod params.q), g ^ z.val) bijective
+    exact exp_bij
+
+
+lemma G1_G2_lemma1 (x : G) (exp : ZMod params.q → G) (exp_bij : Function.Bijective exp) :
+    ∑' (z : ZMod params.q), ite (x = exp z) (1 : ENNReal) 0 = 1 := by
+  obtain ⟨exp_inv, hinv_left, hinv_right⟩ := Function.bijective_iff_has_inverse.mp exp_bij
+  have bij_eq : ∀ (z : ZMod params.q), (x = exp z) ↔ (z = exp_inv x) := by
+    intro z
+    constructor
+    · -- (x = exp z) → (z = exp_inv x)
+      intro h
+      have h1 : exp_inv x = exp_inv (exp z) := congrArg exp_inv h
+      rw [hinv_left z] at h1
+      exact h1.symm
+    · -- (z = exp_inv x) → (x = exp z)
+      intro h
+      have h2 : exp z = exp (exp_inv x) := congrArg exp h
+      rw [hinv_right x] at h2
+      exact h2.symm
+  simp_rw [bij_eq]
+  simp
+
+
+lemma G1_G2_lemma2 (mb : G) :
+    (PMF.uniformOfFintype (ZMod params.q)).bind (fun (z : ZMod params.q) => pure (params.g^z.val * mb)) =
+    (PMF.uniformOfFintype (ZMod params.q)).bind (fun (z : ZMod params.q) => pure (params.g^z.val)) := by
+  ext x
+  simp only [PMF.bind_apply, PMF.uniformOfFintype_apply, Pure.pure]
+  have lhs_eq : ∑' (z : ZMod params.q), ((↑(Fintype.card (ZMod params.q)))⁻¹ : ENNReal) * (PMF.pure (params.g ^ z.val * mb)) x =
+                ((↑(Fintype.card (ZMod params.q)))⁻¹ : ENNReal) * ∑' (z : ZMod params.q), ite (x = params.g ^ z.val * mb) 1 0 := by
+    rw [ENNReal.tsum_mul_left]
+    congr
+    funext z
+    simp only [PMF.pure_apply]
+    split_ifs <;> ring
+  have rhs_eq : ∑' (z : ZMod params.q), ((↑(Fintype.card (ZMod params.q)))⁻¹ : ENNReal) * (PMF.pure (params.g ^ z.val)) x =
+                ((↑(Fintype.card (ZMod params.q)))⁻¹ : ENNReal) * ∑' (z : ZMod params.q), ite (x = params.g ^ z.val) 1 0 := by
+    rw [ENNReal.tsum_mul_left]
+    congr
+    funext z
+    simp only [PMF.pure_apply]
+    split_ifs <;> ring
+  rw [lhs_eq, rhs_eq]
+  rw [G1_G2_lemma1 x (fun z => params.g ^ z.val * mb) (exp_mb_bij mb)]
+  rw [G1_G2_lemma1 x (fun z => params.g ^ z.val) exp_bij]
+
+
+
+lemma G1_G2_lemma3 (m : PMF G) :
+    m.bind (fun (mb : G) => (PMF.uniformOfFintype (ZMod params.q)).bind (fun (z : ZMod params.q) => pure (params.g^z.val * mb))) =
+    (PMF.uniformOfFintype (ZMod params.q)).bind (fun (z : ZMod params.q) => pure (params.g^z.val)) := by
+  simp_rw [G1_G2_lemma2 _]
+  apply bind_skip_const'
+  intro m
+  congr
+
+/-
+  The probability of the attacker (i.e. the composition of A1 and A2)
+  winning Game1 (i.e. guessing the correct bit) is equal to the
+  probability of the attacker winning Game2.
+-/
+theorem Game1_Game2 (A : TwoStageAdversary G G (G × G)) : @Game1 G params A = @Game2 G params A := by
+  simp only [Game1, Game2]
+  apply bind_skip'
+  intro x
+  apply bind_skip'
+  intro y
+  apply bind_skip'
+  intro m
+  apply bind_skip'
+  intro b
+  simp [bind, -PMF.bind_pure, -PMF.bind_bind]
+  simp_rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod params.q))]
+  rw [G1_G2_lemma3]
+
+lemma G2_uniform_lemma (b' : ZMod 2) : (PMF.uniformOfFintype (ZMod 2)).bind (fun (b : ZMod 2) => pure (1 + b + b')) = PMF.uniformOfFintype (ZMod 2) := by
+  -- The function (b ↦ 1 + b + b') is a bijection on ZMod 2
+  have bij : Function.Bijective (fun b : ZMod 2 => 1 + b + b') := by
+    constructor
+    · intro x y hxy
+      have : x + b' = y + b' := by linear_combination hxy
+      linear_combination this
+    · intro y
+      use y - b' - 1
+      ring
+  -- Use the same argument as G1_G2_lemma2
+  ext a
+  simp only [PMF.bind_apply, PMF.uniformOfFintype_apply, Pure.pure, PMF.pure_apply]
+  rw [tsum_fintype]
+  simp only [mul_ite, mul_one, mul_zero]
+  have card_eq : Fintype.card (ZMod 2) = 2 := by norm_num
+  simp only [card_eq]
+  norm_num
+  -- Exactly one value of b makes a = 1 + b + b', namely b = a - b' - 1
+  have : ∃! b : ZMod 2, a = 1 + b + b' := by
+    use a - b' - 1
+    constructor
+    · ring
+    · intro y hy
+      calc y = y + 0 := by ring
+        _ = y + (b' + (a - b' - 1) - (a - 1)) := by ring
+        _ = (y + b') + (a - b' - 1) - (a - 1) := by ring
+        _ = (1 + y + b') + (a - b' - 1) - (1 + a - 1) := by ring
+        _ = a + (a - b' - 1) - a := by rw [← hy]; ring
+        _ = a - b' - 1 := by ring
+  obtain ⟨b₀, hb₀, huniq⟩ := this
+  have sum_eq : ∑ x : ZMod 2, (if a = 1 + x + b' then (2⁻¹ : ENNReal) else 0) = 2⁻¹ := by
+    have : ∑ x : ZMod 2, (if a = 1 + x + b' then (2⁻¹ : ENNReal) else 0) =
+           ∑ x : ZMod 2, (if x = b₀ then (2⁻¹ : ENNReal) else 0) := by
+      congr 1
+      ext x
+      by_cases h : a = 1 + x + b'
+      · simp [h, huniq x h]
+      · simp [h]
+        by_cases hx : x = b₀
+        · subst hx
+          contradiction
+        · simp [hx]
+    rw [this, Finset.sum_ite_eq']
+    simp
+  exact sum_eq
+
+
+/-
+  The probability of the attacker (i.e. the composition of A1 and A2)
+  winning Game2 (i.e. guessing the correct bit) is equal to a coin flip.
+-/
+theorem Game2_uniform (A : TwoStageAdversary G G (G × G)) : @Game2 G params A = PMF.uniformOfFintype (ZMod 2) := by
+  simp [Game2, bind]
+  apply bind_skip_const'
+  intro x
+  apply bind_skip_const'
+  intro m
+  apply bind_skip_const'
+  intro y
+  rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod 2))]
+  simp_rw [PMF.bind_comm (PMF.uniformOfFintype (ZMod 2))]
+  apply bind_skip_const'
+  intro z
+  apply bind_skip_const'
+  intro ζ
+  apply bind_skip_const'
+  intro b'
+  exact G2_uniform_lemma b'
+
+-- parameters (ε : nnreal)
+variable (ε : ENNReal)
+/-
+  The advantage of the attacker (i.e. the composition of A1 and A2) in
+  the semantic security game `ε` is exactly equal to the advantage of D in
+  the Diffie-Hellman game. Therefore, assumining the decisional Diffie-Hellman
+  assumption holds for the group `G`, we conclude `ε` is negligble, and
+  therefore ElGamal is, by definition, semantically secure.
+-/
+
+
+theorem hiding_from_ddh_single_adversary
+    (A : TwoStageAdversary G G (G × G))
+    (DDH_assumption : DDH.Assumption G params.g params.q (D_from_adversary A) ε) :
+    Commitment.comp_hiding_game scheme A 1 - 1/2 ≤ ε := by
+  rw [ComputationalHiding_DDH0]
+  have h : ((PMF.uniformOfFintype (ZMod 2)) 1) = 1/2 := by
+    simp only [PMF.uniformOfFintype_apply, ZMod.card, Nat.cast_ofNat, one_div]
+  rw [← h]
+  rw [← @Game2_uniform G params]
+  rw [← Game1_Game2]
+  rw [Game1_DDH1]
+  exact le_of_eq_of_le rfl DDH_assumption
+
+
+theorem computational_hiding_from_ddh (ε : ENNReal)
+    (DDH_hard : ∀ (D : G → G → G → PMF (ZMod 2)), DDH.Assumption G params.g params.q D ε) :
+    Commitment.computational_hiding (@scheme G params) ε := by
+  unfold Commitment.computational_hiding
+  intro hA
+  apply hiding_from_ddh_single_adversary
+  exact DDH_hard (D_from_adversary hA)
+
+
+end Elgamal