From a73f2587a9a9d77b9ffec3821eec02d94a0c9f30 Mon Sep 17 00:00:00 2001
From: Barry Trager <bmt@us.ibm.com>
Date: Wed, 13 Dec 2023 06:42:18 +0100
Subject: [PATCH] renaming

---
 coq/FHE/zp_prim_root.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/coq/FHE/zp_prim_root.v b/coq/FHE/zp_prim_root.v
index c782e27c..406c4d81 100644
--- a/coq/FHE/zp_prim_root.v
+++ b/coq/FHE/zp_prim_root.v
@@ -452,7 +452,7 @@ Section chinese.
       lia.
   Qed.
       
-  Lemma balanced_chinese_list_mod_1 (l : seq (nat * nat)) :
+  Lemma balanced_chinese_list_mod_inner (l : seq (nat * nat)) :
     (forall p, p \in l -> 0 < p.2) ->
     pairwise coprime (map snd l) ->
     forall p,
@@ -537,7 +537,7 @@ Section chinese.
     by rewrite ltn_pmul2r.
   Qed.
 
-  Lemma balanced_chinese_list_mod_1_lt (l : seq (nat * nat)) :
+  Lemma balanced_chinese_list_mod_inner_lt (l : seq (nat * nat)) :
     uniq l ->
     (forall p, p \in l -> 0 < p.2) ->
     forall p,
@@ -589,7 +589,7 @@ Section chinese.
         apply H in H2.
         lia.
       }
-      rewrite (eqP (balanced_chinese_list_mod_1 posl H0 H1)).
+      rewrite (eqP (balanced_chinese_list_mod_inner posl H0 H1)).
       apply modn_add0.
       rewrite big1_idem //.
       intros.