From 43e08dfe2fd741f728fcfb6f58812601592f2bf8 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 2 Jul 2024 17:37:20 -0400
Subject: [PATCH] Algebra: rename grp_pow_* and reorder one result

---
 theories/Algebra/AbGroups/AbelianGroup.v |  6 ++---
 theories/Algebra/AbGroups/Z.v            |  2 +-
 theories/Algebra/Groups/Group.v          | 32 ++++++++++++------------
 theories/Algebra/Rings/Z.v               | 12 ++++-----
 4 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v
index 1d850ddd8fd..7c9a818bbed 100644
--- a/theories/Algebra/AbGroups/AbelianGroup.v
+++ b/theories/Algebra/AbGroups/AbelianGroup.v
@@ -250,9 +250,9 @@ Proof.
   intros a b.
   induction n; cbn.
   - exact (grp_unit_l _)^.
-  - rewrite 3 grp_pow_int_add_1.
+  - rewrite 3 grp_pow_succ.
     by apply ab_mul_helper.
-  - rewrite 3 grp_pow_int_sub_1.
+  - rewrite 3 grp_pow_pred.
     rewrite (grp_inv_op a b), (commutativity (-b) (-a)).
     by apply ab_mul_helper.
 Defined.
@@ -310,7 +310,7 @@ Proof.
   induction n as [|n IHn] in f, p |- *.
   - reflexivity.
   - rhs nrapply (ap@{Set _} _ (int_of_nat_succ_commute n)).
-    rhs nrapply grp_pow_int_add_1.
+    rhs nrapply grp_pow_succ.
     simpl. f_ap.
     apply IHn.
     intros. apply p.
diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
index 8247d2e3333..1dcde9e0927 100644
--- a/theories/Algebra/AbGroups/Z.v
+++ b/theories/Algebra/AbGroups/Z.v
@@ -30,7 +30,7 @@ Definition grp_pow_homo {G : Group} (g : G)
 Proof.
   snrapply Build_GroupHomomorphism.
   1: exact (grp_pow g).
-  intros m n; apply grp_pow_int_add.
+  intros m n; apply grp_pow_add.
 Defined.
 
 (** The special case for an abelian group, which gives multiplication by an integer. *)
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index dcef27dbb68..39eca032333 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -503,38 +503,38 @@ Defined.
 (** Note that powers don't preserve the group operation as it is not commutative. This does hold in an abelian group so such a result will appear later. *)
 
 (** The next two results tell us how [grp_pow] unfolds. *)
-Definition grp_pow_int_add_1 {G : Group} (n : Int) (g : G)
+Definition grp_pow_succ {G : Group} (n : Int) (g : G)
   : grp_pow g (n.+1)%int = g * grp_pow g n
   := int_iter_succ_l _ _ _.
 
-Definition grp_pow_int_sub_1 {G : Group} (n : Int) (g : G)
+Definition grp_pow_pred {G : Group} (n : Int) (g : G)
   : grp_pow g (n.-1)%int = (- g) * grp_pow g n
   := int_iter_pred_l _ _ _.
 
-(** [grp_pow] commutes negative exponents to powers of the inverse *)
-Definition grp_pow_int_sign_commute {G : Group} (n : Int) (g : G)
-  : grp_pow g (int_neg n) = grp_pow (- g) n.
-Proof.
-  lhs nrapply int_iter_neg.
-  destruct n.
-  - cbn. by rewrite grp_inv_inv.
-  - reflexivity.
-  - reflexivity.
-Defined.
-
 (** [grp_pow] satisfies an additive law of exponents. *)
-Definition grp_pow_int_add {G : Group} (m n : Int) (g : G)
+Definition grp_pow_add {G : Group} (m n : Int) (g : G)
   : grp_pow g (n + m)%int = grp_pow g n * grp_pow g m.
 Proof.
   lhs nrapply int_iter_add.
   induction n; cbn.
   1: exact (grp_unit_l _)^.
-  1: rewrite int_iter_succ_l, grp_pow_int_add_1.
-  2: rewrite int_iter_pred_l, grp_pow_int_sub_1; cbn.
+  1: rewrite int_iter_succ_l, grp_pow_succ.
+  2: rewrite int_iter_pred_l, grp_pow_pred; cbn.
   1,2 : rhs_V srapply associativity;
         apply ap, IHn.
 Defined.
 
+(** [grp_pow] commutes negative exponents to powers of the inverse *)
+Definition grp_pow_neg {G : Group} (n : Int) (g : G)
+  : grp_pow g (int_neg n) = grp_pow (- g) n.
+Proof.
+  lhs nrapply int_iter_neg.
+  destruct n.
+  - cbn. by rewrite grp_inv_inv.
+  - reflexivity.
+  - reflexivity.
+Defined.
+
 (** ** The category of Groups *)
 
 (** ** Groups together with homomorphisms form a 1-category whose equivalences are the group isomorphisms. *)
diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v
index cfe74590276..61f74885f74 100644
--- a/theories/Algebra/Rings/Z.v
+++ b/theories/Algebra/Rings/Z.v
@@ -37,14 +37,14 @@ Proof.
   - simpl.
     by rhs nrapply rng_mult_zero_l.
   - rewrite int_mul_succ_l.
-    rewrite grp_pow_int_add.
-    rewrite grp_pow_int_add_1.
+    rewrite grp_pow_add.
+    rewrite grp_pow_succ.
     rhs nrapply rng_dist_r.
     rewrite rng_mult_one_l.
     f_ap.
   - rewrite int_mul_pred_l.
-    rewrite grp_pow_int_add.
-    rewrite grp_pow_int_sub_1.
+    rewrite grp_pow_add.
+    rewrite grp_pow_pred.
     rhs nrapply rng_dist_r.
     rewrite IHx.
     f_ap.
@@ -72,12 +72,12 @@ Proof.
   unfold rng_homo_int, rng_int_mult; cbn.
   induction x as [|x|x].
   - by rhs nrapply (grp_homo_unit g).
-  - rewrite grp_pow_int_add_1.
+  - rewrite grp_pow_succ.
     change (x.+1%int) with (1 + x)%int.
     rewrite (rng_homo_plus g 1 x).
     rewrite rng_homo_one.
     f_ap.
-  - rewrite grp_pow_int_sub_1.
+  - rewrite grp_pow_pred.
     rewrite IHx.
     clear IHx.
     rewrite <- (rng_homo_one g).