nearest_round_int_odd_abs

IBM · May 22, 2024 · 046ceb3 · 046ceb3
1 parent 953992e
commit 046ceb3
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/coq/FHE/arith.v b/coq/FHE/arith.v
@@ -3012,7 +3012,12 @@ Lemma nearest_round_int_odd_abs (p : nat) (a : int) :
   odd p ->
   `|nearest_round_int a p| = `|nearest_round_int `|a| p|.
 Proof.
-Admitted.
+  intros.
+  destruct a.
+  - by rewrite absz_nat.
+  - rewrite NegzE nearest_round_int_negate //.
+    by rewrite !abszN absz_nat.
+Qed.
 
 Lemma nearest_round_int_leq2 (c p : nat) (a : int) :
   odd p ->