one more tweak

Signed-off-by: Avi Shinnar <shinnar@us.ibm.com>
IBM · May 21, 2024 · 3975f55 · 3975f55
1 parent 51a9d21
commit 3975f55
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/coq/FHE/arith.v b/coq/FHE/arith.v
@@ -2807,7 +2807,7 @@ Lemma nearest_round_int_leq2 (c p : nat) (a : int) :
 Proof.
   intros.
   rewrite /absz.
-
+  case E: nearest_round_int.
   Admitted.
 
 Lemma size_map_poly_le  [aR rR : ringType] [f : aR -> rR] (p : {poly aR}) :