wip

IBM · Mar 1, 2024 · 4395ee4 · 4395ee4
1 parent f9b0582
commit 4395ee4
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/coq/FHE/encode.v b/coq/FHE/encode.v
@@ -1470,6 +1470,10 @@ Proof.
   rewrite coef_Poly.
   case/orP: (leqVgt 3 i)=>ibd.
   - rewrite !(coefD, coefZ, coefC, coefN, coefX, coefXn).
+    replace (i == 2%N) with false by lia.
+    replace (i == 1%N) with false by lia.
+    replace (i == 0%N) with false by lia.
+    rewrite /= mulr0 mulr0n oppr0 !addr0.
     admit.
   - rewrite (nth_map 0); [| by rewrite sz].
     rewrite !(coefD, coefZ, coefC, coefN, coefX, coefXn).