wip

IBM · Jun 3, 2024 · 05d4062 · 05d4062
1 parent 513b5f2
commit 05d4062
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/coq/FHE/arith.v b/coq/FHE/arith.v
@@ -3313,6 +3313,8 @@ Proof.
   assert (pqbig: (1 < p * q)) by lia.
   assert (pno: (Posz p <> 0)) by lia.
   destruct (div_round_mul_ex p (zlift c2 * zlift a) s oddp) as [?[??]].
+  generalize (div_round_add2_perturb_small (zlift c2 * zlift a * s)
+                    (zlift c2 * zlift (- a * q_reduce (p * q) s + q_reduce (p * q) e + q_reduce (p * q) (s ^+ 2 *+ p))) p pno); intros peterb_small.
   exists
     (q_reduce q ( (div_round_add2_perturb (zlift c2 * zlift a * s)
                     (zlift c2 * zlift (- a * q_reduce (p * q) s + q_reduce (p * q) e + q_reduce (p * q) (s ^+ 2 *+ p))) p pno -