cleanup

IBM · Jan 16, 2024 · 566f4b4 · 566f4b4
1 parent 3c5414c
commit 566f4b4
Showing 1 changed file with 3 additions and 9 deletions.
diff --git a/coq/FHE/zp_prim_root.v b/coq/FHE/zp_prim_root.v
@@ -2953,15 +2953,9 @@ Section add_self_pow.
       unfold modn_ord.
       simpl.
       rewrite addrC.
-      f_equal.
-      + apply H.
-        simpl.
-        rewrite (mod_mod_le (i + 2^m)%N le_Sm_n).
-        by rewrite -H2.
-      + apply H.
-        simpl.
-        rewrite (mod_mod_le (j + 2^m)%N le_Sm_n).
-        by rewrite -H1.
+      f_equal; apply H; simpl.
+      + by rewrite (mod_mod_le (i + 2^m)%N le_Sm_n) -H2.
+      + by rewrite (mod_mod_le (j + 2^m)%N le_Sm_n) -H1.
   Qed.
 
   Lemma row_sum_rot_pow_rec_step_preserves_sum {n} (v:'rV[G]_(2^n)) (m : nat)