From b047de41bda2caabfcc47267db018abc290b25b2 Mon Sep 17 00:00:00 2001
From: Barry Trager <bmt@us.ibm.com>
Date: Wed, 29 Nov 2023 22:36:27 +0100
Subject: [PATCH] mat_vec_norm_inf

---
 coq/FHE/encode.v | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/coq/FHE/encode.v b/coq/FHE/encode.v
index 8c1079f6..5b09e976 100644
--- a/coq/FHE/encode.v
+++ b/coq/FHE/encode.v
@@ -1965,12 +1965,13 @@ Section norms.
   Qed.    
     
   Lemma mat_vec_norm_inf {n} (v : 'rV[R[i]]_n) :
-    norm1 v = matrix_norm1 v.
+    norm_inf v = matrix_norm1 v.
   Proof.
-    unfold norm1, matrix_norm1, matrix_norm_inf.
-    symmetry.
-  Admitted.
-
+    rewrite /norm_inf /matrix_norm1 /matrix_norm_inf /=.
+    apply eq_bigr.
+    intros.
+    by rewrite big_ord_recl big_ord0 addr0 mxE.
+  Qed.
 
   Lemma matrix_norm_inf_sub_mult {n m p} 
     (mat1 : 'M[R[i]]_(n, m))