From efe522acfc2a1f0d4be1900a231be8b3fd13d10b Mon Sep 17 00:00:00 2001
From: Barry Trager <bmt@us.ibm.com>
Date: Sat, 28 Oct 2023 18:35:01 +0200
Subject: [PATCH] squeez0

---
 coq/FHE/encode.v | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/coq/FHE/encode.v b/coq/FHE/encode.v
index 39f9047d..0a19d246 100644
--- a/coq/FHE/encode.v
+++ b/coq/FHE/encode.v
@@ -2322,7 +2322,15 @@ Section norms.
     (x <= R0)%O ->
     x = 0.
   Proof.
-    Admitted.
+    intros.
+    apply Rle_antisym.
+    - rewrite /Order.le/= in H0.
+      move /RlebP in H0.
+      by replace (R0) with (IZR (Z0)) in H0 by lra.
+    - rewrite /Order.le/= in H.
+      move /RlebP in H.
+      by replace (R0) with (IZR (Z0)) in H by lra.
+  Qed.
 
   Lemma canon_norm_zer_mod_qpoly n (p : {poly R}) :
     canon_norm_inf n p = 0 ->