From e6e4e7b5aa309fb8b65eea25968b534c10efeb26 Mon Sep 17 00:00:00 2001
From: Barry Trager <bmt@us.ibm.com>
Date: Fri, 1 Dec 2023 13:01:30 +0100
Subject: [PATCH] wip

---
 coq/FHE/encode.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/coq/FHE/encode.v b/coq/FHE/encode.v
index a32ac69e..f579bd2f 100644
--- 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.