wip

IBM · Apr 23, 2024 · 3b5d6d7 · 3b5d6d7
1 parent 4152363
commit 3b5d6d7
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/coq/FHE/arith.v b/coq/FHE/arith.v
@@ -2271,6 +2271,15 @@ Lemma nearest_round_int_le (n1 n2 d : int) :
   `|n1| <= `|n2| ->
                  `|nearest_round_int n1 d| <= `|nearest_round_int n2 d|.
 Proof.
+  intros.
+  rewrite /nearest_round_int /nearest_round /ran_round.
+  case: (Order.lt).
+  - case: Order.lt.
+    + admit.
+    + admit.
+  - case: Order.lt.
+    + admit.
+    + admit.
   Admitted.
 
 Lemma div_round_eq (p : nat) (a : {poly int}) :