wip

IBM · Dec 1, 2023 · e6e4e7b · e6e4e7b
1 parent 454a137
commit e6e4e7b
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/coq/FHE/encode.v b/coq/FHE/encode.v
@@ -2270,6 +2270,14 @@ Section norms.
       ((matrix_norm_inf mat1) * (matrix_norm_inf mat2)).
   Proof.
     rewrite /matrix_norm_inf /mulmx /=.
+    generalize (@max_mult_distr n); intros.
+    rewrite /mul /= in H.
+    rewrite H.
+    - apply bigmax_le2.
+      intros.
+      under eq_bigr do rewrite mxE.
+
+
   Admitted.