diff --git a/coq/FHE/encode.v b/coq/FHE/encode.v
index 318e1bcf..cbe3e01c 100644
--- a/coq/FHE/encode.v
+++ b/coq/FHE/encode.v
@@ -1953,8 +1953,7 @@ Section norms.
     - generalize (diag_mx_is_diag v) => H.
       move /is_diag_mxP in H.
       intros.
-      rewrite -tr_diag_mx mxE.
-      rewrite H //.
+      rewrite H; [|rewrite eq_sym //].
       by rewrite ComplexField.Normc.normc0.
   Qed.
 
@@ -1967,10 +1966,9 @@ Section norms.
     - by rewrite /diag_mx mxE eq_refl /= mulr1n.
     - intros.
       rewrite mxE.
-      Admitted.
-(*
-      by rewrite ComplexField.Normc.normc0.
-*)
+      rewrite eq_sym (Bool.negb_involutive_reverse (@eq_op (Finite.eqType (ordinal_finType n)) i0 i)).
+      by rewrite H ComplexField.Normc.normc0.
+ Qed.
 
   Lemma normc_nneg (x : R[i]) :
     (R0  <= normc x)%O.