From 56f37f397dbe4d843eb12052316b6a260435429c Mon Sep 17 00:00:00 2001
From: Giuseppe <8973725+Eagle941@users.noreply.github.com>
Date: Wed, 13 Mar 2024 21:55:21 +0000
Subject: [PATCH] Fixed gates

---
 ProvenZk/Gates.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/ProvenZk/Gates.lean b/ProvenZk/Gates.lean
index 777abc5..8eb3d73 100644
--- a/ProvenZk/Gates.lean
+++ b/ProvenZk/Gates.lean
@@ -43,10 +43,9 @@ def ne (a b : ZMod N): Prop := a ≠ b
 
 def le_8 (a b : ZMod N): Prop :=
   ∃z w: Fin (binary_length N), z.val % N = a.val ∧ w.val % N = b.val ∧
-  a.val <= b.val
+  z.val <= w.val
 
 def le_9 (a b : ZMod N): Prop :=
-  ∃z w: Fin (binary_length N), z.val = a.val ∧ w.val = b.val ∧
   a.val <= b.val
 
 def to_binary (a : ZMod N) (d : Nat) (out : Vector (ZMod N) d): Prop :=