finish proof of size_charpoly

Signed-off-by: Avi Shinnar <[email protected]>
IBM · Feb 29, 2024 · 0c90d53 · 0c90d53
1 parent 80a9774
commit 0c90d53
Showing 1 changed file with 4 additions and 4 deletions.
diff --git a/coq/FHE/encode.v b/coq/FHE/encode.v
@@ -1288,12 +1288,12 @@ Proof.
   - rewrite size_addl.
     + rewrite size_scale.
       * rewrite size_polyX //.
-      * admit.
+      * by rewrite -eqr_opp opprK oppr0.
     + rewrite size_scale.
       * rewrite size_polyX size_polyC.
-        case : (eqVneq (cnorm c) 0); rewrite //.  
-      * admit.
-Admitted.
+        case : (eqVneq (cnorm c) 0); rewrite //.
+      * by rewrite -eqr_opp opprK oppr0.
+Qed.
 
 Lemma characteristic_polynomial_correct (c : R[i]) :
   (map_poly RtoC (characteristic_polynomial c)).[c] = 0.