matrix_vec_norm_inf_sub_mult

IBM · Dec 1, 2023 · c1946af · c1946af
1 parent c9ce3b6
commit c1946af
Showing 1 changed file with 2 additions and 3 deletions.
diff --git a/coq/FHE/encode.v b/coq/FHE/encode.v
@@ -2257,9 +2257,8 @@ Section norms.
     - apply bigmax_le2.
       intros.
       rewrite big_ord_recl big_ord0 addr0 mxE /trmx /=.
-      generalize (@mat_vec_norm_bound1 n m mat vec j); intros.
-      symmetry; under eq_bigr do rewrite !mxE.
-                                 by rewrite H0.
+      under eq_bigr do rewrite !mxE.
+                       by rewrite mat_vec_norm_bound1.
     - apply /RlebP.
       apply bigmax_normc_nneg.
   Qed.