From a98c258b0949aeca78e70454430b037d0aa157fe Mon Sep 17 00:00:00 2001
From: Barry Trager <bmt@us.ibm.com>
Date: Wed, 22 May 2024 14:26:23 -0400
Subject: [PATCH] wip

---
 coq/FHE/arith.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/coq/FHE/arith.v b/coq/FHE/arith.v
index e8e9d4e7..f2d318a9 100644
--- a/coq/FHE/arith.v
+++ b/coq/FHE/arith.v
@@ -3027,8 +3027,12 @@ Proof.
   intros.
   assert (Posz p != 0) by lia.
   generalize (nearest_round_int_le_const_nat _ _ _ H1 H0); intros.
-  rewrite /absz.
-  case E: (nearest_round_int a p).
+  rewrite nearest_round_int_odd_abs //.
+  assert (p != 0%N) by lia.
+  assert  ((0 : int) <= `|a|)%O by lia.
+  generalize (nearest_round_int_pos p `|a| H3 H4); intros.
+  rewrite {1}/absz.
+  case E: (nearest_round_int `|a| p).
   - admit.
   - admit.
   Admitted.