From 109eea170ce15b1eed5afe75732ae115646b0f0c Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Fri, 28 Jun 2024 16:56:14 +0200
Subject: [PATCH 01/14] switch to Int in cring_Z

Signed-off-by: Ali Caglayan <alizter@gmail.com>

<!-- ps-id: eb524d2a-9345-45cd-9bd3-34c4a5dff4cd -->
---
 theories/Algebra/AbGroups/Cyclic.v    |   4 +-
 theories/Algebra/AbGroups/Z.v         |  16 +-
 theories/Algebra/Rings/Z.v            | 291 ++++++++------------------
 theories/HIT/FreeIntQuotient.v        |   6 +-
 theories/Homotopy/PinSn.v             |   2 +-
 theories/Spaces/Circle.v              |  76 +++----
 theories/Spaces/Int.v                 | 189 ++++++++++++++++-
 theories/Spaces/Torus/TorusHomotopy.v |   4 +-
 8 files changed, 312 insertions(+), 276 deletions(-)

diff --git a/theories/Algebra/AbGroups/Cyclic.v b/theories/Algebra/AbGroups/Cyclic.v
index af7c790d92e..7c658022c05 100644
--- a/theories/Algebra/AbGroups/Cyclic.v
+++ b/theories/Algebra/AbGroups/Cyclic.v
@@ -1,6 +1,6 @@
 Require Import Basics Types WildCat.Core Truncations.Core
   AbelianGroup AbHom Centralizer AbProjective
-  Groups.FreeGroup AbGroups.Z BinInt.Core Spaces.Int.
+  Groups.FreeGroup AbGroups.Z Spaces.Int.
 
 (** * Cyclic groups *)
 
@@ -71,7 +71,7 @@ Defined.
 
 (** The map sending the generator to [1 : Int]. *)
 Definition Z1_to_Z `{Funext} : ab_Z1 $-> abgroup_Z
-  := Z1_rec (G:=abgroup_Z) 1%binint.
+  := Z1_rec (G:=abgroup_Z) 1%int.
 
 (** TODO:  Prove that [Z1_to_Z] is a group isomorphism. *)
 
diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
index 6eb290a44b9..57a0a837e94 100644
--- a/theories/Algebra/AbGroups/Z.v
+++ b/theories/Algebra/AbGroups/Z.v
@@ -1,5 +1,5 @@
 Require Import Basics.
-Require Import Spaces.Pos.Core Spaces.BinInt.
+Require Import Spaces.Pos.Core Spaces.Int.
 Require Import Algebra.AbGroups.AbelianGroup.
 
 Local Set Universe Minimization ToSet.
@@ -8,17 +8,17 @@ Local Set Universe Minimization ToSet.
 
 (** See also Cyclic.v for a definition of the integers as the free group on one generator. *)
 
-Local Open Scope binint_scope.
+Local Open Scope int_scope.
 
 (** TODO: switch to [Int] *)
 Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
   snrapply Build_AbGroup.
-  - refine (Build_Group BinInt binint_add 0 binint_negation _); repeat split.
+  - refine (Build_Group Int int_add 0 int_neg _); repeat split.
     + exact _.
-    + exact binint_add_assoc.
-    + exact binint_add_0_r.
-    + exact binint_add_negation_l.
-    + exact binint_add_negation_r.
-  - exact binint_add_comm.
+    + exact int_add_assoc.
+    + exact int_add_0_r.
+    + exact int_add_neg_l.
+    + exact int_add_neg_r.
+  - exact int_add_comm.
 Defined.
diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v
index ee0a10a886e..c9cd2a9619e 100644
--- a/theories/Algebra/Rings/Z.v
+++ b/theories/Algebra/Rings/Z.v
@@ -1,7 +1,7 @@
 Require Import Classes.interfaces.canonical_names.
 Require Import Algebra.AbGroups.
 Require Import Algebra.Rings.CRing.
-Require Import Spaces.BinInt Spaces.Pos.
+Require Import Spaces.Int Spaces.Pos.
 Require Import WildCat.Core.
 
 (** In this file we define the ring Z of integers. The underlying abelian group is already defined in Algebra.AbGroups.Z. Many of the ring axioms are proven and made opaque. Typically, everything inside IsCRing can be opaque since we will only ever rewrite along them and they are hprops. This also means we don't have to be too careful with how our proofs are structured. This allows us to freely use tactics such as rewrite. It would perhaps be possible to shorten many of the proofs here, but it would probably be unneeded due to the opacicty. *)
@@ -10,155 +10,52 @@ Require Import WildCat.Core.
 Definition cring_Z : CRing.
 Proof.
   snrapply Build_CRing'.
+  6: repeat split.
   - exact abgroup_Z.
-  - exact 1%binint.
-  - exact binint_mul.
-  - exact binint_mul_comm.
-  - exact binint_mul_add_distr_l.
-  - split.
-    + split.
-      * exact _.
-      * exact binint_mul_assoc.
-    + exact binint_mul_1_l.
-    + exact binint_mul_1_r.
+  - exact 1%int.
+  - exact int_mul.
+  - exact int_mul_comm.
+  - exact int_dist_l.
+  - exact _.
+  - exact int_mul_assoc.
+  - exact int_mul_1_l.
+  - exact int_mul_1_r.
 Defined.
 
 Local Open Scope mc_scope.
 
 (** Multiplication of a ring element by an integer. *)
-(** We call this a "catamorphism" which is the name of the map from an initial object. It seems to be a more common terminology in computer science. *)
-Definition cring_catamorphism_fun (R : CRing) (z : cring_Z) : R
-  := match z with
-     | neg z => pos_peano_rec R (-1) (fun n nr => -1 + nr) z
-     | 0%binint => 0
-     | pos z => pos_peano_rec R 1 (fun n nr => 1 + nr) z
-     end.
-
-(** TODO: remove these (they will be cleaned up in the future)*)
-(** Left multiplication is an equivalence *)
-Local Instance isequiv_group_left_op {G} `{IsGroup G}
-  : forall (x : G), IsEquiv (fun t => sg_op x t).
-Proof.
-  intro x.
-  srapply isequiv_adjointify.
-  1: exact (sg_op (-x)).
-  all: intro y.
-  all: refine (associativity _ _ _ @ _ @ left_identity y).
-  all: refine (ap (fun x => x * y) _).
-  1: apply right_inverse.
-  apply left_inverse.
-Defined.
-
-(** Right multiplication is an equivalence *)
-Local Instance isequiv_group_right_op {G} `{IsGroup G}
-  : forall x:G, IsEquiv (fun y => sg_op y x).
-Proof.
-  intro x.
-  srapply isequiv_adjointify.
-  1: exact (fun y => sg_op y (- x)).
-  all: intro y.
-  all: refine ((associativity _ _ _)^ @ _ @ right_identity y).
-  all: refine (ap (y *.) _).
-  1: apply left_inverse.
-  apply right_inverse.
-Defined.
+Definition rng_int_mult (R : Ring) (z : cring_Z) : R
+  := int_iter (fun x => 1 + x) z 0.
 
 (** Preservation of + *)
-Global Instance issemigrouppreserving_cring_catamorphism_fun_plus (R : CRing)
-  : IsSemiGroupPreserving (Aop:=cring_plus) (Bop:=cring_plus)
-      (cring_catamorphism_fun R : cring_Z -> R).
+Global Instance issemigrouppreserving_plus_rng_int_mult (R : Ring)
+  : IsSemiGroupPreserving (Aop:=(+)) (Bop:=(+)) (rng_int_mult R).
 Proof.
-  (** Unfortunately, due to how we have defined things we need to seperate this out into 9 cases. *)
-  hnf. intros [x| |x] [y| |y].
-  (** Some of these cases are easy however *)
-  2,5,8: cbn; by rewrite right_identity.
-  3,4: symmetry; apply left_identity.
-  (** This leaves us with four cases to consider *)
-  (** x < 0 , y < 0 *)
-  { change (cring_catamorphism_fun R ((neg x) + (neg y))%binint
-      = (cring_catamorphism_fun R (neg x)) + (cring_catamorphism_fun R (neg y))).
-    induction y as [|y IHy] using pos_peano_ind.
-    { simpl.
-      rewrite pos_add_1_r.
-      rewrite pos_peano_rec_beta_pos_succ.
-      apply commutativity. }
-    simpl.
-    rewrite pos_add_succ_r.
-    rewrite 2 pos_peano_rec_beta_pos_succ.
-    rewrite simple_associativity.
-    rewrite (commutativity _ (-1)).
-    rewrite <- simple_associativity.
-    f_ap. }
-  (** x < 0 , y > 0 *)
-  { cbn.
-    revert x.
-    induction y as [|y IHy] using pos_peano_ind; intro x.
-    { cbn.
-      induction x as [|x] using pos_peano_ind.
-      1: symmetry; cbn; apply left_inverse.
-      rewrite pos_peano_rec_beta_pos_succ.
-      rewrite binint_pos_sub_succ_r.
-      cbn; rewrite <- simple_associativity.
-      apply (rng_moveL_Vr (R:=R)).
-      apply commutativity. }
-    induction x as [|x IHx] using pos_peano_ind.
-    { rewrite binint_pos_sub_succ_l.
-      cbn; apply (rng_moveL_Vr (R:=R)).
-      by rewrite pos_peano_rec_beta_pos_succ. }
-    rewrite binint_pos_sub_succ_succ.
-    rewrite IHy.
-    rewrite 2 pos_peano_rec_beta_pos_succ.
-    rewrite (commutativity (-1)).
-    rewrite simple_associativity.
-    rewrite <- (simple_associativity _ _ 1).
-    rewrite left_inverse.
-    f_ap.
-    symmetry.
-    apply right_identity. }
+  intros x y.
+  induction x as [|x|x].
+  - simpl.
+    rhs nrapply left_identity.
+    2: exact _.
+    reflexivity.
   - cbn.
-    revert x.
-    induction y as [|y IHy] using pos_peano_ind; intro x.
-    { induction x as [|x] using pos_peano_ind.
-      1: symmetry; cbn; apply right_inverse.
-      rewrite pos_peano_rec_beta_pos_succ.
-      rewrite (commutativity 1).
-      rewrite <- simple_associativity.
-      rewrite binint_pos_sub_succ_l.
-      cbn; by rewrite right_inverse, right_identity. }
-    induction x as [|x IHx] using pos_peano_ind.
-    { rewrite binint_pos_sub_succ_r.
-      rewrite pos_peano_rec_beta_pos_succ.
-      rewrite simple_associativity.
-      cbn.
-      rewrite (right_inverse 1).
-      symmetry.
-      apply left_identity. }
-    rewrite binint_pos_sub_succ_succ.
-    rewrite IHy.
-    rewrite 2 pos_peano_rec_beta_pos_succ.
-    rewrite (commutativity 1).
-    rewrite simple_associativity.
-    rewrite <- (simple_associativity _ _ (-1)).
-    rewrite (right_inverse 1).
-    f_ap; symmetry.
-    apply right_identity.
+    rewrite int_add_succ_l.
+    unfold rng_int_mult.
+    rewrite 2 int_iter_succ_l.
+    rhs_V nrapply simple_associativity.
+    2: exact _.
+    f_ap.
   - cbn.
-    induction y as [|y IHy] using pos_peano_ind.
-    { cbn.
-      rewrite pos_add_1_r.
-      rewrite pos_peano_rec_beta_pos_succ.
-      apply commutativity. }
-    rewrite pos_add_succ_r.
-    rewrite 2 pos_peano_rec_beta_pos_succ.
-    rewrite simple_associativity.
-    rewrite IHy.
-    rewrite simple_associativity.
-    rewrite (commutativity 1).
-    reflexivity.
-Qed.
+    rewrite int_add_pred_l.
+    unfold rng_int_mult.
+    rewrite 2 int_iter_pred_l.
+    rhs_V nrapply simple_associativity.
+    2: exact _.
+    f_ap.
+Defined.
 
-Lemma cring_catamorphism_fun_negate {R} x
-  : cring_catamorphism_fun R (- x) = - cring_catamorphism_fun R x.
+Lemma rng_int_mult_neg {R} x
+  : rng_int_mult R (- x) = - rng_int_mult R x.
 Proof.
   snrapply (groups.preserves_negate _).
   1-6: typeclasses eauto.
@@ -167,59 +64,44 @@ Proof.
   split.
 Defined.
 
-Lemma cring_catamorphism_fun_pos_mult {R} x y
-  : cring_catamorphism_fun R (pos x * pos y)%binint
-    = cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y).
-Proof.
-  revert y.
-  induction x as [|x IHx] using pos_peano_ind; intro y.
-  { symmetry.
-    apply left_identity. }
-  change (cring_catamorphism_fun R (pos (pos_succ x * y)%pos)
-    = cring_catamorphism_fun R (pos (pos_succ x)) * cring_catamorphism_fun R (pos y)).
-  rewrite pos_mul_succ_l.
-  refine (issemigrouppreserving_cring_catamorphism_fun_plus
-    R (pos (x * y)%pos) (pos y) @ _).
-  rewrite IHx.
-  transitivity ((1 + cring_catamorphism_fun R (pos x)) * cring_catamorphism_fun R (pos y)).
-  2: simpl; by rewrite pos_peano_rec_beta_pos_succ.
-  rewrite (rng_dist_r (A:=R)).
-  rewrite rng_mult_one_l.
-  apply commutativity.
-Qed.
-
 (** Preservation of * (multiplication) *)
-Global Instance issemigrouppreserving_cring_catamorphism_fun_mult (R : CRing)
-  : IsSemiGroupPreserving (Aop:=(.*.)) (Bop:=(.*.))
-      (cring_catamorphism_fun R : cring_Z -> R).
+Global Instance issemigrouppreserving_mult_rng_int_mult (R : Ring)
+  : IsSemiGroupPreserving (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R).
 Proof.
-  hnf. intros [x| |x] [y| |y].
-  2,5,8: symmetry; apply (rng_mult_zero_r (A:=R)).
-  3,4: cbn; symmetry; rewrite (commutativity 0); apply (rng_mult_zero_r (A:=R)).
-  { change (cring_catamorphism_fun R (pos (x * y)%pos)
-      = cring_catamorphism_fun R (- (pos x : cring_Z))
-        * cring_catamorphism_fun R (- (pos y : cring_Z))).
-    by rewrite 2 cring_catamorphism_fun_negate, cring_catamorphism_fun_pos_mult,
-      (rng_mult_negate_negate (A:=R)). }
-  { change (cring_catamorphism_fun R (- (pos (x * y)%pos : cring_Z))
-      = cring_catamorphism_fun R (- (pos x : cring_Z))
-        * cring_catamorphism_fun R (pos y)).
-    by rewrite 2 cring_catamorphism_fun_negate, cring_catamorphism_fun_pos_mult,
-      (rng_mult_negate_l (A:=R)). }
-  { change (cring_catamorphism_fun R (- (pos (x * y)%pos : cring_Z))
-      = cring_catamorphism_fun R (pos x)
-        * cring_catamorphism_fun R (- (pos y : cring_Z))).
-    by rewrite 2 cring_catamorphism_fun_negate, cring_catamorphism_fun_pos_mult,
-      (rng_mult_negate_r (A:=R)). }
-  apply cring_catamorphism_fun_pos_mult.
-Qed.
+  intros x y.
+  induction x as [|x|x].
+  - simpl.
+    by rhs nrapply rng_mult_zero_l.
+  - cbn.
+    rewrite int_mul_succ_l.
+    rewrite issemigrouppreserving_plus_rng_int_mult.
+    unfold rng_int_mult in *.
+    rewrite int_iter_succ_l.
+    rhs nrapply rng_dist_r.
+    rewrite rng_mult_one_l.
+    rewrite IHx.
+    reflexivity.
+  - cbn.
+    rewrite int_mul_pred_l.
+    rewrite issemigrouppreserving_plus_rng_int_mult.
+    unfold rng_int_mult in *.
+    rewrite int_iter_pred_l.
+    rhs nrapply rng_dist_r.
+    rewrite IHx.
+    f_ap.
+    lhs rapply rng_int_mult_neg.
+    symmetry; apply rng_mult_negate.
+Defined.
 
 (** This is a ring homomorphism *)
-Definition rng_homo_int (R : CRing) : cring_Z $-> R.
+Definition rng_homo_int (R : Ring) : (cring_Z : Ring) $-> R.
 Proof.
   snrapply Build_RingHomomorphism.
-  1: exact (cring_catamorphism_fun R).
-  repeat split; exact _.
+  1: exact (rng_int_mult R).
+  repeat split.
+  1,2: exact _.
+  hnf.
+  apply rng_plus_zero_r.
 Defined.
 
 (** The integers are the initial commutative ring *)
@@ -229,28 +111,21 @@ Proof.
   intro R.
   exists (rng_homo_int R).
   intros g x.
-  destruct x as [n| |p].
-  + induction n using pos_peano_ind.
-    { cbn. symmetry; rapply (rng_homo_minus_one (B:=R)). }
-    simpl.
-    rewrite pos_peano_rec_beta_pos_succ.
-    rewrite binint_neg_pos_succ.
-    unfold binint_pred.
-    rewrite binint_add_comm.
-    rewrite rng_homo_plus.
-    rewrite rng_homo_minus_one.
-    apply ap.
-    exact IHn.
-  + by rewrite 2 rng_homo_zero.
-  + induction p using pos_peano_ind.
-    { cbn. symmetry; rapply (rng_homo_one g). }
-    simpl.
-    rewrite pos_peano_rec_beta_pos_succ.
-    rewrite binint_pos_pos_succ.
-    unfold binint_succ.
-    rewrite binint_add_comm.
-    rewrite rng_homo_plus.
+  induction x as [|x|x].
+  - by rhs nrapply (grp_homo_unit g).
+  - unfold rng_homo_int, rng_int_mult; cbn.
+    rewrite int_iter_succ_l.
+    change (x.+1%int) with (1 + x)%int.
+    rewrite (rng_homo_plus g 1 x).
     rewrite rng_homo_one.
-    apply ap.
-    exact IHp.
+    f_ap.
+  - unfold rng_homo_int, rng_int_mult in IHx |- *; cbn in IHx |- *.
+    rewrite int_iter_pred_l.
+    cbn.
+    rewrite IHx.
+    clear IHx.
+    rewrite <- (rng_homo_one g).
+    rewrite <- (rng_homo_negate g).
+    lhs_V nrapply (rng_homo_plus g).
+    f_ap.
 Defined.
diff --git a/theories/HIT/FreeIntQuotient.v b/theories/HIT/FreeIntQuotient.v
index 096248ad933..f80293dc40b 100644
--- a/theories/HIT/FreeIntQuotient.v
+++ b/theories/HIT/FreeIntQuotient.v
@@ -1,6 +1,6 @@
 (* -*- mode: coq; mode: visual-line -*- *)
 Require Import HoTT.Basics HoTT.Types.
-Require Import Spaces.BinInt Spaces.Circle.
+Require Import Spaces.Int Spaces.Circle.
 Require Import Colimits.Coeq HIT.Flattening Truncations.Core Truncations.Connectedness.
 
 Local Open Scope path_scope.
@@ -16,8 +16,8 @@ Section FreeIntAction.
 
   (** A free action by [Int] is the same as a single autoequivalence [f] (the action of [1]) whose iterates are all pointwise distinct. *)
   Context (f : R <~> R)
-          (f_free : forall (r : R) (n m : BinInt),
-                      (binint_iter f n r = binint_iter f m r) -> (n = m)).
+          (f_free : forall (r : R) (n m : Int),
+                      (int_iter f n r = int_iter f m r) -> (n = m)).
 
   (** We can then define the quotient to be the coequalizer of [f] and the identity map.  This gives it the desired universal property for all types; it remains to show that this definition gives a set. *)
   Let RmodZ := Coeq f idmap.
diff --git a/theories/Homotopy/PinSn.v b/theories/Homotopy/PinSn.v
index a81b460163d..4b76b93f9fc 100644
--- a/theories/Homotopy/PinSn.v
+++ b/theories/Homotopy/PinSn.v
@@ -2,7 +2,7 @@ Require Import Basics Types.
 Require Import WildCat.
 Require Import Pointed.
 Require Import Truncations.Core Truncations.Connectedness.
-Require Import Spaces.BinInt Spaces.Circle Spaces.Spheres.
+Require Import Spaces.Int Spaces.Circle Spaces.Spheres.
 Require Import Algebra.AbGroups.
 Require Import Homotopy.HomotopyGroup.
 Require Import Homotopy.HSpaceS1.
diff --git a/theories/Spaces/Circle.v b/theories/Spaces/Circle.v
index 840b3392393..ba4bf1f75ea 100644
--- a/theories/Spaces/Circle.v
+++ b/theories/Spaces/Circle.v
@@ -2,7 +2,7 @@
 Require Import Basics Types.
 Require Import Pointed.Core Pointed.Loops Pointed.pEquiv.
 Require Import HSet.
-Require Import Spaces.Pos Spaces.BinInt.
+Require Import Spaces.Int.
 Require Import Colimits.Coeq.
 Require Import Truncations.Core Truncations.Connectedness.
 
@@ -90,11 +90,11 @@ Section EncodeDecode.
 
   (** First we define the type of codes, this is a type family over the circle. This can be thought of as the covering space by the homotopical real numbers. It is defined by mapping loop to the path given by univalence applied to the automorphism of the integers. We will show that the section of this family at [base] is equivalent to the loop space of the circle. Giving us an equivalence [base = base <~> Int]. *)
   Definition Circle_code : Circle -> Type
-    := Circle_rec Type BinInt (path_universe binint_succ).
+    := Circle_rec Type Int (path_universe int_succ).
 
   (** Transporting along [loop] gives us the successor automorphism on [Int]. *)
-  Definition transport_Circle_code_loop (z : BinInt)
-    : transport Circle_code loop z = binint_succ z.
+  Definition transport_Circle_code_loop (z : Int)
+    : transport Circle_code loop z = int_succ z.
   Proof.
     refine (transport_compose idmap Circle_code loop z @ _).
     unfold Circle_code; rewrite Circle_rec_beta_loop.
@@ -102,13 +102,13 @@ Section EncodeDecode.
   Defined.
 
   (** Transporting along [loop^] gives us the predecessor on [Int]. *)
-  Definition transport_Circle_code_loopV (z : BinInt)
-    : transport Circle_code loop^ z = binint_pred z.
+  Definition transport_Circle_code_loopV (z : Int)
+    : transport Circle_code loop^ z = int_pred z.
   Proof.
     refine (transport_compose idmap Circle_code loop^ z @ _).
     rewrite ap_V.
     unfold Circle_code; rewrite Circle_rec_beta_loop.
-    rewrite <- (path_universe_V binint_succ).
+    rewrite <- (path_universe_V int_succ).
     apply transport_path_universe.
   Defined.
 
@@ -125,52 +125,26 @@ Section EncodeDecode.
     refine (transport_arrow _ _ _ @ _).
     refine (transport_paths_r loop _ @ _).
     rewrite transport_Circle_code_loopV.
-    destruct z as [n| |n].
-    2: apply concat_Vp.
-    { rewrite <- binint_neg_pos_succ.
-      unfold loopexp, loopexp_pos.
-      rewrite pos_peano_ind_beta_pos_succ.
-      apply concat_pV_p. }
-    induction n as [|n nH] using pos_peano_ind.
-    1: apply concat_1p.
-    rewrite <- pos_add_1_r.
-    change (pos (n + 1)%pos)
-      with (binint_succ (pos n)).
-    rewrite binint_pred_succ.
-    cbn; rewrite pos_add_1_r.
-    unfold loopexp_pos.
-    rewrite pos_peano_ind_beta_pos_succ.
-    reflexivity.
+    rewrite loopexp_pred_r.
+    apply concat_pV_p.
   Defined.
 
   (** The non-trivial part of the proof that decode and encode are equivalences is showing that decoding followed by encoding is the identity on the fibers over [base]. *)
-  Definition Circle_encode_loopexp (z:BinInt)
+  Definition Circle_encode_loopexp (z : Int)
     : Circle_encode base (loopexp loop z) = z.
   Proof.
-    destruct z as [n | | n]; unfold Circle_encode.
-    - induction n using pos_peano_ind; simpl in *.
-      + refine (moveR_transport_V _ loop _ _ _).
-        by symmetry; apply transport_Circle_code_loop.
-      + unfold loopexp_pos.
-        rewrite pos_peano_ind_beta_pos_succ.
-        rewrite transport_pp.
-        refine (moveR_transport_V _ loop _ _ _).
-        refine (_ @ (transport_Circle_code_loop _)^).
-        refine (IHn @ _^).
-        rewrite binint_neg_pos_succ.
-        by rewrite binint_succ_pred.
+    induction z as [|n | n].
     - reflexivity.
-    - induction n using pos_peano_ind; simpl in *.
-      + by apply transport_Circle_code_loop.
-      + unfold loopexp_pos.
-        rewrite pos_peano_ind_beta_pos_succ.
-        rewrite transport_pp.
-        refine (moveR_transport_p _ loop _ _ _).
-        refine (_ @ (transport_Circle_code_loopV _)^).
-        refine (IHn @ _^).
-        rewrite <- pos_add_1_r.
-        change (binint_pred (binint_succ (pos n)) = pos n).
-        apply binint_pred_succ.
+    - rewrite loopexp_succ_r.
+      unfold Circle_encode in IHz |- *.
+      rewrite transport_pp.
+      rewrite IHz.
+      apply transport_Circle_code_loop.
+    - rewrite loopexp_pred_r.
+      unfold Circle_encode in IHz |- *.
+      rewrite transport_pp.
+      rewrite IHz.
+      apply transport_Circle_code_loopV.
   Defined.
 
   (** Now we put it together. *)
@@ -187,7 +161,7 @@ Section EncodeDecode.
   Defined.
 
   (** Finally giving us an equivalence between the loop space of the [Circle] and [Int]. *)
-  Definition equiv_loopCircle_int : (base = base) <~> BinInt
+  Definition equiv_loopCircle_int : (base = base) <~> Int
     := Build_Equiv _ _ (Circle_encode base) (Circle_encode_isequiv base).
 
 End EncodeDecode.
@@ -215,15 +189,15 @@ Proof.
   assert (q := merely_path_is0connected Circle base y).
   strip_truncations.
   destruct p, q.
-  refine (istrunc_equiv_istrunc (n := 0) BinInt equiv_loopCircle_int^-1).
+  refine (istrunc_equiv_istrunc (n := 0) Int equiv_loopCircle_int^-1).
 Defined.
 
 (** ** Iteration of equivalences *)
 
 (** If [P : Circle -> Type] is defined by a type [X] and an autoequivalence [f], then the image of [n : Int] regarded as in [base = base] is [iter_int f n]. *)
-Definition Circle_action_is_iter `{Univalence} X (f : X <~> X) (n : BinInt) (x : X)
+Definition Circle_action_is_iter `{Univalence} X (f : X <~> X) (n : Int) (x : X)
 : transport (Circle_rec Type X (path_universe f)) (equiv_loopCircle_int^-1 n) x
-  = binint_iter f n x.
+  = int_iter f n x.
 Proof.
   refine (_ @ loopexp_path_universe _ _ _).
   refine (transport_compose idmap _ _ _ @ _).
diff --git a/theories/Spaces/Int.v b/theories/Spaces/Int.v
index c7327614602..9b30a6cc68e 100644
--- a/theories/Spaces/Int.v
+++ b/theories/Spaces/Int.v
@@ -1,4 +1,4 @@
-Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences.
+Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe.
 Require Basics.Numerals.Decimal.
 Require Import Spaces.Nat.Core.
 
@@ -140,6 +140,11 @@ Defined.
 (** By Hedberg's theorem, we have that the integers are a set. *)
 Global Instance ishset_int@{} : IsHSet Int := _.
 
+(** *** Pointedness *)
+
+(** We sometimes want to treat the integers as a pointed type with basepoint given by 0. *)
+Global Instance ispointed_int : IsPointed Int := 0.
+
 (** ** Operations *)
 
 (** *** Addition *)
@@ -526,3 +531,185 @@ Proof.
     rewrite <- int_mul_neg_l.
     by rewrite IHx.
 Defined.
+
+(** ** Iteration of equivalences *)
+
+(** *** Iteration by arbitrary integers *)
+
+Definition int_iter {A} (f : A -> A) `{!IsEquiv f} (n : Int) : A -> A
+  := match n with
+      | negS n => fun x => nat_iter n.+1%nat f^-1 x
+      | zero => idmap
+      | posS n => fun x => nat_iter n.+1%nat f x
+     end.
+
+(** Iteration by arbitrary integers requires the endofunction to be an equivalence, so that we can define a negative iteration by using its inverse. *)
+
+Definition int_iter_succ_l {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
+  : int_iter f (int_succ n) a = f (int_iter f n a).
+Proof.
+  induction n as [|n|n].
+  - reflexivity.
+  - by destruct n.
+  - rewrite int_pred_succ. 
+    destruct n.
+    1: symmetry; apply eisretr.
+    by rhs nrapply eisretr.
+Defined.
+
+Definition int_iter_succ_r {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
+  : int_iter f (int_succ n) a = int_iter f n (f a).
+Proof.
+  induction n as [|n|n].
+  - reflexivity.
+  - destruct n.
+    1: reflexivity.
+    cbn; f_ap.
+  - destruct n.
+    1: symmetry; apply eissect.
+    rewrite int_pred_succ.
+    apply (ap f^-1).
+    rewrite <- int_neg_pred in IHn.
+    rhs_V nrapply IHn.
+    by destruct n.
+Defined.
+
+Definition int_iter_pred_l {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
+  : int_iter f (int_pred n) a = f^-1 (int_iter f n a).
+Proof.
+  induction n as [|n|n].
+  - reflexivity.
+  - rewrite int_succ_pred.
+    apply moveR_equiv_M in IHn.
+    lhs_V nrapply IHn.
+    destruct n.
+    1: exact (eisretr f _ @ (eissect f _)^).
+    destruct n; by rhs nrapply eissect.
+  - by destruct n.
+Defined.
+
+Definition int_iter_pred_r {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
+  : int_iter f (int_pred n) a = int_iter f n (f^-1 a).
+Proof.
+  induction n as [|n|n].
+  - reflexivity.
+  - rewrite int_succ_pred.
+    destruct n.
+    1: symmetry; nrapply eisretr.
+    cbn; f_ap.
+    by destruct n.
+  - destruct n.
+    1: reflexivity.
+    cbn; f_ap.
+Defined.
+
+Definition int_iter_add {A} (f : A -> A) `{IsEquiv _ _ f} (m n : Int)
+  : int_iter f (m + n) == int_iter f m o int_iter f n.
+Proof.
+  intros a.
+  induction m as [|m|m].
+  - reflexivity.
+  - rewrite int_add_succ_l.
+    rewrite 2 int_iter_succ_l.
+    f_ap.
+  - rewrite int_add_pred_l.
+    rewrite 2 int_iter_pred_l.
+    f_ap.
+Defined.
+
+(** ** Exponentiation of loops *)
+
+Definition loopexp {A : Type} {x : A} (p : x = x) (z : Int) : (x = x)
+  := int_iter (equiv_concat_r p x) z idpath.
+
+Definition loopexp_succ_r {A : Type} {x : A} (p : x = x) (z : Int)
+  : loopexp p z.+1 = loopexp p z @ p
+  := int_iter_succ_l _ _ _.
+
+Definition loopexp_pred_r {A : Type} {x : A} (p : x = x) (z : Int)
+  : loopexp p z.-1 = loopexp p z @ p^
+  := int_iter_pred_l _ _ _.
+
+Definition loopexp_succ_l {A : Type} {x : A} (p : x = x) (z : Int)
+  : loopexp p z.+1 = p @ loopexp p z.
+Proof.
+  rewrite loopexp_succ_r.
+  induction z as [|z|z].
+  - exact (concat_1p _ @ (concat_p1 _)^).
+  - rewrite loopexp_succ_r.
+    rhs nrapply concat_p_pp.
+    f_ap.
+  - rewrite loopexp_pred_r.
+    lhs nrapply concat_pV_p.
+    rhs nrapply concat_p_pp.
+    by apply moveL_pV.
+Defined.
+
+Definition loopexp_pred_l {A : Type} {x : A} (p : x = x) (z : Int)
+  : loopexp p z.-1 = p^ @ loopexp p z.
+Proof.
+  rewrite loopexp_pred_r.
+  induction z as [|z|z].
+  - exact (concat_1p _ @ (concat_p1 _)^).
+  - rewrite loopexp_succ_r.
+    lhs nrapply concat_pp_V.
+    rhs nrapply concat_p_pp.
+    by apply moveL_pM.
+  - rewrite loopexp_pred_r.
+    rhs nrapply concat_p_pp.
+    f_ap.
+Defined.
+
+Definition ap_loopexp {A B} (f : A -> B) {x : A} (p : x = x) (z : Int)
+  : ap f (loopexp p z) = loopexp (ap f p) z.
+Proof.
+  induction z as [|z|z].
+  - reflexivity.
+  - rewrite 2 loopexp_succ_l.
+    cbn; lhs nrapply ap_pp.
+    f_ap.
+  - rewrite 2 loopexp_pred_l.
+    cbn; lhs nrapply ap_pp.
+    f_ap.
+    apply ap_V.
+Defined.
+
+Definition loopexp_add {A : Type} {x : A} (p : x = x) a b
+  : loopexp p (a + b) = loopexp p a @ loopexp p b.
+Proof.
+  induction a as [|a|a].
+  - symmetry; apply concat_1p.
+  - rewrite int_add_succ_l.
+    rewrite 2 loopexp_succ_l.
+    by rewrite IHa, concat_p_pp.
+  - rewrite int_add_pred_l.
+    rewrite 2 loopexp_pred_l.
+    by rewrite IHa, concat_p_pp.
+Defined.
+
+(** Under univalence, exponentiation of loops corresponds to iteration of autoequivalences. *)
+
+Definition equiv_path_loopexp {A : Type} (p : A = A) (z : Int) (a : A)
+  : equiv_path A A (loopexp p z) a = int_iter (equiv_path A A p) z a.
+Proof.
+  induction z as [|z|z].
+  - reflexivity.
+  - rewrite loopexp_succ_r.
+    cbn; rewrite transport_pp.
+    rewrite int_iter_succ_l.
+    f_ap.
+  - rewrite loopexp_pred_r.
+    cbn; rewrite transport_pp.
+    rewrite int_iter_pred_l.
+    f_ap.
+Defined.
+
+Definition loopexp_path_universe `{Univalence} {A : Type} (f : A <~> A)
+  (z : Int) (a : A)
+  : transport idmap (loopexp (path_universe f) z) a = int_iter f z a.
+Proof.
+  revert f. equiv_intro (equiv_path A A) p.
+  refine (_ @ equiv_path_loopexp p z a).
+  refine (ap (fun q => equiv_path A A (loopexp q z) a) _).
+  apply eissect.
+Defined.
diff --git a/theories/Spaces/Torus/TorusHomotopy.v b/theories/Spaces/Torus/TorusHomotopy.v
index 46bedc1da48..ef20a811351 100644
--- a/theories/Spaces/Torus/TorusHomotopy.v
+++ b/theories/Spaces/Torus/TorusHomotopy.v
@@ -4,7 +4,7 @@ Require Import Modalities.ReflectiveSubuniverse Truncations.Core.
 Require Import Algebra.AbGroups.
 Require Import Homotopy.HomotopyGroup.
 Require Import Homotopy.PinSn.
-Require Import Spaces.BinInt.Core Spaces.Circle.
+Require Import Spaces.Int Spaces.Circle.
 
 Require Import Spaces.Torus.Torus.
 Require Import Spaces.Torus.TorusEquivCircles.
@@ -55,7 +55,7 @@ Proof.
 Defined.
 
 (** Loop space of torus *)
-Theorem loops_torus `{Univalence} : loops T <~>* BinInt * BinInt.
+Theorem loops_torus `{Univalence} : loops T <~>* Int * Int.
 Proof.
   (* Since [T] is 1-truncated, [loops T] is 0-truncated, and is therefore equivalent to its 0-truncation. *)
   refine (_ o*E pequiv_ptr (n:=0)).

From 9bfde5669d70ece2990440c88825ce67c56b06ad Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Fri, 28 Jun 2024 17:12:25 +0200
Subject: [PATCH 02/14] fix test

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 test/Algebra/Rings/Matrix.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/Algebra/Rings/Matrix.v b/test/Algebra/Rings/Matrix.v
index 5c70cfbf768..88632a6dfab 100644
--- a/test/Algebra/Rings/Matrix.v
+++ b/test/Algebra/Rings/Matrix.v
@@ -1,7 +1,7 @@
 From HoTT Require Import Basics.
 From HoTT Require Import Algebra.Rings.Matrix.
 From HoTT Require Import Spaces.Nat.Core Spaces.List.Core.
-From HoTT Require Import Algebra.Rings.Z Spaces.BinInt.Core Algebra.Rings.CRing.
+From HoTT Require Import Algebra.Rings.Z Spaces.Int Algebra.Rings.CRing.
 From HoTT Require Import Classes.interfaces.canonical_names.
 
 Local Open Scope mc_scope.
@@ -38,7 +38,7 @@ Definition test2_B := Build_Matrix' nat 4 4
 
 Definition test2 : entries test2_A = entries test2_B := idpath.
 
-Local Open Scope binint_scope.
+Local Open Scope int_scope.
 
 (** Matrices with ring entries can be multiplied *)
 

From 2a34b75b61526be1819b63154206eba0b4acfd5e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thomas=20Wilskow=20Thorbj=C3=B8rnsen?=
 <thomas.w.thorbjornsen@gmail.com>
Date: Fri, 28 Jun 2024 11:45:39 -0400
Subject: [PATCH 03/14] Commuting lemma for int_iter

---
 theories/Spaces/Int.v | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/theories/Spaces/Int.v b/theories/Spaces/Int.v
index 9b30a6cc68e..46c5823df13 100644
--- a/theories/Spaces/Int.v
+++ b/theories/Spaces/Int.v
@@ -617,6 +617,39 @@ Proof.
     f_ap.
 Defined.
 
+(** This is a general lemma about commutativity of monoid units. Don't know what file this should belong to. *)
+Lemma inverse_commute_commute {A} (f : A -> A) `{!IsEquiv f} (g : A -> A) (p : g o f == f o g)
+  : g o f^-1 == f^-1 o g.
+Proof.
+  intros a.
+  lhs_V apply (eissect f ((g o f^-1) a)).
+  lhs_V apply (ap f^-1 (p (f^-1 a))).
+  lhs apply (ap (f^-1 o g) (eisretr f a)).
+  reflexivity.
+Defined.
+
+(** If the maps f and g commutes, then the order of application doesn't matter *)
+Definition int_iter_commute_function_application {A} (f : A -> A) `{!IsEquiv f} (g : A -> A) (p : g o f == f o g) (n : Int) (a : A)
+  : g (int_iter f n a) = int_iter f n (g a).
+Proof.
+  destruct n.
+  - induction n.
+    + simpl.
+      exact (inverse_commute_commute f g p a).
+    + simpl.
+      lhs apply (inverse_commute_commute f g p).
+      lhs apply (ap f^-1 IHn).
+      reflexivity.
+  - reflexivity.
+  - induction n.
+    + simpl.
+      exact (p a).
+    + simpl.
+      lhs apply p.
+      lhs apply (ap f IHn).
+      reflexivity.
+Defined.
+
 (** ** Exponentiation of loops *)
 
 Definition loopexp {A : Type} {x : A} (p : x = x) (z : Int) : (x = x)

From 13987641d767f337eaf724fe3db0e32fb4f7a16e Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Fri, 28 Jun 2024 18:20:15 +0200
Subject: [PATCH 04/14] simplify int_iter_comm

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Spaces/Int.v | 40 +++++++++++++---------------------------
 1 file changed, 13 insertions(+), 27 deletions(-)

diff --git a/theories/Spaces/Int.v b/theories/Spaces/Int.v
index 46c5823df13..0be2ec02f61 100644
--- a/theories/Spaces/Int.v
+++ b/theories/Spaces/Int.v
@@ -617,37 +617,23 @@ Proof.
     f_ap.
 Defined.
 
-(** This is a general lemma about commutativity of monoid units. Don't know what file this should belong to. *)
-Lemma inverse_commute_commute {A} (f : A -> A) `{!IsEquiv f} (g : A -> A) (p : g o f == f o g)
-  : g o f^-1 == f^-1 o g.
-Proof.
-  intros a.
-  lhs_V apply (eissect f ((g o f^-1) a)).
-  lhs_V apply (ap f^-1 (p (f^-1 a))).
-  lhs apply (ap (f^-1 o g) (eisretr f a)).
-  reflexivity.
-Defined.
-
 (** If the maps f and g commutes, then the order of application doesn't matter *)
-Definition int_iter_commute_function_application {A} (f : A -> A) `{!IsEquiv f} (g : A -> A) (p : g o f == f o g) (n : Int) (a : A)
+Definition int_iter_commute_function_application {A} (f : A -> A) `{!IsEquiv f}
+  (g : A -> A) (p : g o f == f o g) (n : Int) (a : A)
   : g (int_iter f n a) = int_iter f n (g a).
 Proof.
-  destruct n.
-  - induction n.
-    + simpl.
-      exact (inverse_commute_commute f g p a).
-    + simpl.
-      lhs apply (inverse_commute_commute f g p).
-      lhs apply (ap f^-1 IHn).
-      reflexivity.
+  induction n as [|n IHn|n IHn] in a |- *.
   - reflexivity.
-  - induction n.
-    + simpl.
-      exact (p a).
-    + simpl.
-      lhs apply p.
-      lhs apply (ap f IHn).
-      reflexivity.
+  - rewrite 2 int_iter_succ_r.
+    rewrite IHn.
+    f_ap.
+  - rewrite 2 int_iter_pred_r.
+    rewrite IHn.
+    f_ap.
+    apply moveL_equiv_V.
+    lhs_V nrapply p.
+    f_ap.
+    apply eisretr.
 Defined.
 
 (** ** Exponentiation of loops *)

From f91be4cdc403f41e92bf907be75b781772f54aeb Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 29 Jun 2024 13:53:54 -0400
Subject: [PATCH 05/14] Rings/Z.v, Int.v: some cleanups

---
 theories/Algebra/Rings/Z.v |  3 +-
 theories/Spaces/Int.v      | 59 ++++++++++++++++++--------------------
 2 files changed, 30 insertions(+), 32 deletions(-)

diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v
index c9cd2a9619e..67a6c3b851a 100644
--- a/theories/Algebra/Rings/Z.v
+++ b/theories/Algebra/Rings/Z.v
@@ -24,7 +24,8 @@ Defined.
 
 Local Open Scope mc_scope.
 
-(** Multiplication of a ring element by an integer. *)
+(** Every ring has a unique ring map from the integers. *)
+(** TODO: rename? *)
 Definition rng_int_mult (R : Ring) (z : cring_Z) : R
   := int_iter (fun x => 1 + x) z 0.
 
diff --git a/theories/Spaces/Int.v b/theories/Spaces/Int.v
index 0be2ec02f61..3629fdd9b7f 100644
--- a/theories/Spaces/Int.v
+++ b/theories/Spaces/Int.v
@@ -536,6 +536,8 @@ Defined.
 
 (** *** Iteration by arbitrary integers *)
 
+(** Iteration by arbitrary integers requires the endofunction to be an equivalence, so that we can define a negative iteration by using its inverse. *)
+
 Definition int_iter {A} (f : A -> A) `{!IsEquiv f} (n : Int) : A -> A
   := match n with
       | negS n => fun x => nat_iter n.+1%nat f^-1 x
@@ -543,7 +545,11 @@ Definition int_iter {A} (f : A -> A) `{!IsEquiv f} (n : Int) : A -> A
       | posS n => fun x => nat_iter n.+1%nat f x
      end.
 
-(** Iteration by arbitrary integers requires the endofunction to be an equivalence, so that we can define a negative iteration by using its inverse. *)
+Definition int_iter_neg {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
+  : int_iter f (- n) a = int_iter f^-1 n a.
+Proof.
+  by destruct n.
+Defined.
 
 Definition int_iter_succ_l {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
   : int_iter f (int_succ n) a = f (int_iter f n a).
@@ -553,8 +559,7 @@ Proof.
   - by destruct n.
   - rewrite int_pred_succ. 
     destruct n.
-    1: symmetry; apply eisretr.
-    by rhs nrapply eisretr.
+    all: symmetry; apply eisretr.
 Defined.
 
 Definition int_iter_succ_r {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
@@ -569,7 +574,6 @@ Proof.
     1: symmetry; apply eissect.
     rewrite int_pred_succ.
     apply (ap f^-1).
-    rewrite <- int_neg_pred in IHn.
     rhs_V nrapply IHn.
     by destruct n.
 Defined.
@@ -577,30 +581,23 @@ Defined.
 Definition int_iter_pred_l {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
   : int_iter f (int_pred n) a = f^-1 (int_iter f n a).
 Proof.
-  induction n as [|n|n].
-  - reflexivity.
-  - rewrite int_succ_pred.
-    apply moveR_equiv_M in IHn.
-    lhs_V nrapply IHn.
-    destruct n.
-    1: exact (eisretr f _ @ (eissect f _)^).
-    destruct n; by rhs nrapply eissect.
-  - by destruct n.
+  (* Convert the problem to be a problem about [f^-1] and [-n]. *)
+  lhs_V exact (int_iter_neg f^-1 (n.-1) a).
+  rhs_V exact (ap f^-1 (int_iter_neg f^-1 n a)).
+  (* Then [int_iter_succ_l] applies, after changing [- n.-1] to [(-n).+1]. *)
+  rewrite int_neg_pred.
+  apply int_iter_succ_l.
 Defined.
 
 Definition int_iter_pred_r {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
   : int_iter f (int_pred n) a = int_iter f n (f^-1 a).
 Proof.
-  induction n as [|n|n].
-  - reflexivity.
-  - rewrite int_succ_pred.
-    destruct n.
-    1: symmetry; nrapply eisretr.
-    cbn; f_ap.
-    by destruct n.
-  - destruct n.
-    1: reflexivity.
-    cbn; f_ap.
+  (* Convert the problem to be a problem about [f^-1] and [-n]. *)
+  lhs_V exact (int_iter_neg f^-1 (n.-1) a).
+  rhs_V exact (int_iter_neg f^-1 n (f^-1 a)).
+  (* Then [int_iter_succ_r] applies, after changing [- n.-1] to [(-n).+1]. *)
+  rewrite int_neg_pred.
+  apply int_iter_succ_r.
 Defined.
 
 Definition int_iter_add {A} (f : A -> A) `{IsEquiv _ _ f} (m n : Int)
@@ -617,7 +614,7 @@ Proof.
     f_ap.
 Defined.
 
-(** If the maps f and g commutes, then the order of application doesn't matter *)
+(** If the maps [f] and [g] commute, then the order of application doesn't matter *)
 Definition int_iter_commute_function_application {A} (f : A -> A) `{!IsEquiv f}
   (g : A -> A) (p : g o f == f o g) (n : Int) (a : A)
   : g (int_iter f n a) = int_iter f n (g a).
@@ -652,9 +649,9 @@ Definition loopexp_pred_r {A : Type} {x : A} (p : x = x) (z : Int)
 Definition loopexp_succ_l {A : Type} {x : A} (p : x = x) (z : Int)
   : loopexp p z.+1 = p @ loopexp p z.
 Proof.
-  rewrite loopexp_succ_r.
+  lhs nrapply loopexp_succ_r.
   induction z as [|z|z].
-  - exact (concat_1p _ @ (concat_p1 _)^).
+  - nrapply concat_1p_p1.
   - rewrite loopexp_succ_r.
     rhs nrapply concat_p_pp.
     f_ap.
@@ -693,17 +690,17 @@ Proof.
     apply ap_V.
 Defined.
 
-Definition loopexp_add {A : Type} {x : A} (p : x = x) a b
-  : loopexp p (a + b) = loopexp p a @ loopexp p b.
+Definition loopexp_add {A : Type} {x : A} (p : x = x) m n
+  : loopexp p (m + n) = loopexp p m @ loopexp p n.
 Proof.
-  induction a as [|a|a].
+  induction m as [|m|m].
   - symmetry; apply concat_1p.
   - rewrite int_add_succ_l.
     rewrite 2 loopexp_succ_l.
-    by rewrite IHa, concat_p_pp.
+    by rewrite IHm, concat_p_pp.
   - rewrite int_add_pred_l.
     rewrite 2 loopexp_pred_l.
-    by rewrite IHa, concat_p_pp.
+    by rewrite IHm, concat_p_pp.
 Defined.
 
 (** Under univalence, exponentiation of loops corresponds to iteration of autoequivalences. *)

From 0c92bcddbae76d8dab2ac0364564c26fa088837a Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sat, 29 Jun 2024 14:29:13 -0400
Subject: [PATCH 06/14] Int.v: generalize/rename int_iter_commute_map and use
 twice

---
 theories/Spaces/Int.v | 33 ++++++++++-----------------------
 1 file changed, 10 insertions(+), 23 deletions(-)

diff --git a/theories/Spaces/Int.v b/theories/Spaces/Int.v
index 3629fdd9b7f..6b4a8130b99 100644
--- a/theories/Spaces/Int.v
+++ b/theories/Spaces/Int.v
@@ -614,10 +614,11 @@ Proof.
     f_ap.
 Defined.
 
-(** If the maps [f] and [g] commute, then the order of application doesn't matter *)
-Definition int_iter_commute_function_application {A} (f : A -> A) `{!IsEquiv f}
-  (g : A -> A) (p : g o f == f o g) (n : Int) (a : A)
-  : g (int_iter f n a) = int_iter f n (g a).
+(** If [g : A -> A'] commutes with automorphisms of [A] and [A'], then it commutes with iteration. *)
+Definition int_iter_commute_map {A A'} (f : A -> A) `{!IsEquiv f}
+  (f' : A' -> A') `{!IsEquiv f'}
+  (g : A -> A') (p : g o f == f' o g) (n : Int) (a : A)
+  : g (int_iter f n a) = int_iter f' n (g a).
 Proof.
   induction n as [|n IHn|n IHn] in a |- *.
   - reflexivity.
@@ -679,15 +680,8 @@ Defined.
 Definition ap_loopexp {A B} (f : A -> B) {x : A} (p : x = x) (z : Int)
   : ap f (loopexp p z) = loopexp (ap f p) z.
 Proof.
-  induction z as [|z|z].
-  - reflexivity.
-  - rewrite 2 loopexp_succ_l.
-    cbn; lhs nrapply ap_pp.
-    f_ap.
-  - rewrite 2 loopexp_pred_l.
-    cbn; lhs nrapply ap_pp.
-    f_ap.
-    apply ap_V.
+  nrapply int_iter_commute_map.
+  intro q; apply ap_pp.
 Defined.
 
 Definition loopexp_add {A : Type} {x : A} (p : x = x) m n
@@ -708,16 +702,9 @@ Defined.
 Definition equiv_path_loopexp {A : Type} (p : A = A) (z : Int) (a : A)
   : equiv_path A A (loopexp p z) a = int_iter (equiv_path A A p) z a.
 Proof.
-  induction z as [|z|z].
-  - reflexivity.
-  - rewrite loopexp_succ_r.
-    cbn; rewrite transport_pp.
-    rewrite int_iter_succ_l.
-    f_ap.
-  - rewrite loopexp_pred_r.
-    cbn; rewrite transport_pp.
-    rewrite int_iter_pred_l.
-    f_ap.
+  refine (int_iter_commute_map _ _ (fun p => equiv_path A A p a) _ _ _).
+  intro q; cbn.
+  nrapply transport_pp.
 Defined.
 
 Definition loopexp_path_universe `{Univalence} {A : Type} (f : A <~> A)

From 061a7adecf25c154c625ebc7bdc9716c83ab0ff2 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Sat, 29 Jun 2024 23:49:47 +0200
Subject: [PATCH 07/14] generalse rng_int_mult to arb elements and split
 IsMonoidPres proof

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/Rings/Z.v | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v
index 67a6c3b851a..25444f32bab 100644
--- a/theories/Algebra/Rings/Z.v
+++ b/theories/Algebra/Rings/Z.v
@@ -26,12 +26,12 @@ Local Open Scope mc_scope.
 
 (** Every ring has a unique ring map from the integers. *)
 (** TODO: rename? *)
-Definition rng_int_mult (R : Ring) (z : cring_Z) : R
-  := int_iter (fun x => 1 + x) z 0.
+Definition rng_int_mult (R : Ring) (r : R) (z : cring_Z) : R
+  := int_iter (fun x => r + x) z 0.
 
 (** Preservation of + *)
 Global Instance issemigrouppreserving_plus_rng_int_mult (R : Ring)
-  : IsSemiGroupPreserving (Aop:=(+)) (Bop:=(+)) (rng_int_mult R).
+  : IsSemiGroupPreserving (Aop:=(+)) (Bop:=(+)) (rng_int_mult R 1).
 Proof.
   intros x y.
   induction x as [|x|x].
@@ -55,19 +55,23 @@ Proof.
     f_ap.
 Defined.
 
+Global Instance isunitpreserving_plus_rng_int_mult (R : Ring)
+  : IsUnitPreserving (Aunit:=zero) (Bunit:= canonical_names.zero) (rng_int_mult R 1)
+  := idpath.
+
+Global Instance ismonoidpreserving_plus_rng_int_mult (R : Ring)
+  : IsMonoidPreserving (Aop:=(+)) (Bop:=(+)) (rng_int_mult R 1)
+  := {}.
+
 Lemma rng_int_mult_neg {R} x
-  : rng_int_mult R (- x) = - rng_int_mult R x.
+  : rng_int_mult R 1 (- x) = - rng_int_mult R 1 x.
 Proof.
-  snrapply (groups.preserves_negate _).
-  1-6: typeclasses eauto.
-  snrapply Build_IsMonoidPreserving.
-  1: exact _.
-  split.
+  snrapply (groups.preserves_negate _); exact _.
 Defined.
 
 (** Preservation of * (multiplication) *)
 Global Instance issemigrouppreserving_mult_rng_int_mult (R : Ring)
-  : IsSemiGroupPreserving (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R).
+  : IsSemiGroupPreserving (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R 1).
 Proof.
   intros x y.
   induction x as [|x|x].
@@ -98,7 +102,7 @@ Defined.
 Definition rng_homo_int (R : Ring) : (cring_Z : Ring) $-> R.
 Proof.
   snrapply Build_RingHomomorphism.
-  1: exact (rng_int_mult R).
+  1: exact (rng_int_mult R 1).
   repeat split.
   1,2: exact _.
   hnf.

From 47f2da2a5057a2ec5920030bf7732210e0719adb Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sun, 30 Jun 2024 08:37:03 -0400
Subject: [PATCH 08/14] Rings/Z.v: generalize results about rng_int_mult;
 update comments

---
 theories/Algebra/Rings/Z.v | 30 ++++++++++++++++--------------
 1 file changed, 16 insertions(+), 14 deletions(-)

diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v
index 25444f32bab..44fcaf88e3a 100644
--- a/theories/Algebra/Rings/Z.v
+++ b/theories/Algebra/Rings/Z.v
@@ -4,7 +4,7 @@ Require Import Algebra.Rings.CRing.
 Require Import Spaces.Int Spaces.Pos.
 Require Import WildCat.Core.
 
-(** In this file we define the ring Z of integers. The underlying abelian group is already defined in Algebra.AbGroups.Z. Many of the ring axioms are proven and made opaque. Typically, everything inside IsCRing can be opaque since we will only ever rewrite along them and they are hprops. This also means we don't have to be too careful with how our proofs are structured. This allows us to freely use tactics such as rewrite. It would perhaps be possible to shorten many of the proofs here, but it would probably be unneeded due to the opacicty. *)
+(** * In this file we define the ring [cring_Z] of integers with underlying abelian group [abroup_Z] defined in Algebra.AbGroups.Z. We also define multiplication by an integer in a general ring, and show that [cring_Z] is initial. *)
 
 (** The ring of integers *)
 Definition cring_Z : CRing.
@@ -24,14 +24,13 @@ Defined.
 
 Local Open Scope mc_scope.
 
-(** Every ring has a unique ring map from the integers. *)
-(** TODO: rename? *)
+(** Every ring element can be multiplied by an integer. *)
 Definition rng_int_mult (R : Ring) (r : R) (z : cring_Z) : R
   := int_iter (fun x => r + x) z 0.
 
-(** Preservation of + *)
-Global Instance issemigrouppreserving_plus_rng_int_mult (R : Ring)
-  : IsSemiGroupPreserving (Aop:=(+)) (Bop:=(+)) (rng_int_mult R 1).
+(** [rng_int_mult R r] preserves addition. *)
+Global Instance issemigrouppreserving_plus_rng_int_mult (R : Ring) (r : R)
+  : IsSemiGroupPreserving (Aop:=(+)) (Bop:=(+)) (rng_int_mult R r).
 Proof.
   intros x y.
   induction x as [|x|x].
@@ -55,21 +54,24 @@ Proof.
     f_ap.
 Defined.
 
-Global Instance isunitpreserving_plus_rng_int_mult (R : Ring)
-  : IsUnitPreserving (Aunit:=zero) (Bunit:= canonical_names.zero) (rng_int_mult R 1)
+(** [rng_int_mult R r] sends [0 : Int] to [0 : R] definitionally. *)
+Global Instance isunitpreserving_plus_rng_int_mult (R : Ring) (r : R)
+  : IsUnitPreserving (Aunit:=zero) (Bunit:=canonical_names.zero) (rng_int_mult R r)
   := idpath.
 
-Global Instance ismonoidpreserving_plus_rng_int_mult (R : Ring)
-  : IsMonoidPreserving (Aop:=(+)) (Bop:=(+)) (rng_int_mult R 1)
+(** [rng_int_mult R r] preserves addition and zero. *)
+Global Instance ismonoidpreserving_plus_rng_int_mult (R : Ring) (r : R)
+  : IsMonoidPreserving (Aop:=(+)) (Bop:=(+)) (rng_int_mult R r)
   := {}.
 
-Lemma rng_int_mult_neg {R} x
-  : rng_int_mult R 1 (- x) = - rng_int_mult R 1 x.
+(** [rng_int_mult R r] commutes with negation. *)
+Lemma rng_int_mult_neg (R : Ring) (r : R) x
+  : rng_int_mult R r (- x) = - rng_int_mult R r x.
 Proof.
   snrapply (groups.preserves_negate _); exact _.
 Defined.
 
-(** Preservation of * (multiplication) *)
+(** [rng_int_mult R 1] preserves multiplication.  This requires that the specified ring element is the unit. *)
 Global Instance issemigrouppreserving_mult_rng_int_mult (R : Ring)
   : IsSemiGroupPreserving (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R 1).
 Proof.
@@ -98,7 +100,7 @@ Proof.
     symmetry; apply rng_mult_negate.
 Defined.
 
-(** This is a ring homomorphism *)
+(** [rng_int_mult R 1] is a ring homomorphism *)
 Definition rng_homo_int (R : Ring) : (cring_Z : Ring) $-> R.
 Proof.
   snrapply Build_RingHomomorphism.

From c125988618e6ab33cc3220eaabeb7c6124016f77 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Sun, 30 Jun 2024 15:39:45 +0200
Subject: [PATCH 09/14] generalise and move rng_int_mult for abgroup

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/AbGroups/Z.v | 32 ++++++++++++++++
 theories/Algebra/Rings/Z.v    | 69 +++++++----------------------------
 2 files changed, 45 insertions(+), 56 deletions(-)

diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
index 57a0a837e94..727e72361e3 100644
--- a/theories/Algebra/AbGroups/Z.v
+++ b/theories/Algebra/AbGroups/Z.v
@@ -22,3 +22,35 @@ Proof.
     + exact int_add_neg_r.
   - exact int_add_comm.
 Defined.
+
+Local Open Scope mc_scope.
+
+(** Every element of an abelian group can be multiplied by an integer. *)
+Definition abgroup_int_mult (A : AbGroup) (x : A) (z : abgroup_Z) : A
+  := grp_pow x z.
+
+(** [abgroup_int_mult A r] preserves addition. *)
+Global Instance issemigrouppreserving_plus_abgroup_int_mult (A : AbGroup) (x : A)
+  : IsSemiGroupPreserving (Aop:=(+)) (Bop:=(+)) (abgroup_int_mult A x).
+Proof.
+  intros y z.
+  apply grp_pow_int_add.
+Defined.
+
+(** [abgroup_int_mult A r] sends [0 : Int] to [0 : R] definitionally. *)
+Global Instance isunitpreserving_plus_abgroup_int_mult (A : AbGroup) (x : A)
+  : IsUnitPreserving (Aunit:=zero) (Bunit:=canonical_names.zero)
+      (abgroup_int_mult A x)
+  := idpath.
+
+(** [abgroup_int_mult R r] preserves addition and zero. *)
+Global Instance ismonoidpreserving_plus_abgroup_int_mult (A : AbGroup) (x : A)
+  : IsMonoidPreserving (Aop:=(+)) (Bop:=(+)) (abgroup_int_mult A x)
+  := {}.
+
+(** [abgroup_int_mult R r] commutes with negation. *)
+Definition abgroup_int_mult_neg (A : AbGroup) (x : A) z
+  : abgroup_int_mult A x (- z) = - abgroup_int_mult A x z.
+Proof.
+  snrapply (groups.preserves_negate _); exact _.
+Defined.
diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v
index 44fcaf88e3a..cd22b4a5a89 100644
--- a/theories/Algebra/Rings/Z.v
+++ b/theories/Algebra/Rings/Z.v
@@ -24,56 +24,11 @@ Defined.
 
 Local Open Scope mc_scope.
 
-(** Every ring element can be multiplied by an integer. *)
-Definition rng_int_mult (R : Ring) (r : R) (z : cring_Z) : R
-  := int_iter (fun x => r + x) z 0.
-
-(** [rng_int_mult R r] preserves addition. *)
-Global Instance issemigrouppreserving_plus_rng_int_mult (R : Ring) (r : R)
-  : IsSemiGroupPreserving (Aop:=(+)) (Bop:=(+)) (rng_int_mult R r).
-Proof.
-  intros x y.
-  induction x as [|x|x].
-  - simpl.
-    rhs nrapply left_identity.
-    2: exact _.
-    reflexivity.
-  - cbn.
-    rewrite int_add_succ_l.
-    unfold rng_int_mult.
-    rewrite 2 int_iter_succ_l.
-    rhs_V nrapply simple_associativity.
-    2: exact _.
-    f_ap.
-  - cbn.
-    rewrite int_add_pred_l.
-    unfold rng_int_mult.
-    rewrite 2 int_iter_pred_l.
-    rhs_V nrapply simple_associativity.
-    2: exact _.
-    f_ap.
-Defined.
-
-(** [rng_int_mult R r] sends [0 : Int] to [0 : R] definitionally. *)
-Global Instance isunitpreserving_plus_rng_int_mult (R : Ring) (r : R)
-  : IsUnitPreserving (Aunit:=zero) (Bunit:=canonical_names.zero) (rng_int_mult R r)
-  := idpath.
-
-(** [rng_int_mult R r] preserves addition and zero. *)
-Global Instance ismonoidpreserving_plus_rng_int_mult (R : Ring) (r : R)
-  : IsMonoidPreserving (Aop:=(+)) (Bop:=(+)) (rng_int_mult R r)
-  := {}.
-
-(** [rng_int_mult R r] commutes with negation. *)
-Lemma rng_int_mult_neg (R : Ring) (r : R) x
-  : rng_int_mult R r (- x) = - rng_int_mult R r x.
-Proof.
-  snrapply (groups.preserves_negate _); exact _.
-Defined.
+Definition rng_int_mult (R : Ring) := abgroup_int_mult R. 
 
 (** [rng_int_mult R 1] preserves multiplication.  This requires that the specified ring element is the unit. *)
 Global Instance issemigrouppreserving_mult_rng_int_mult (R : Ring)
-  : IsSemiGroupPreserving (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R 1).
+  : IsSemiGroupPreserving (A:=cring_Z) (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R 1).
 Proof.
   intros x y.
   induction x as [|x|x].
@@ -81,22 +36,24 @@ Proof.
     by rhs nrapply rng_mult_zero_l.
   - cbn.
     rewrite int_mul_succ_l.
-    rewrite issemigrouppreserving_plus_rng_int_mult.
     unfold rng_int_mult in *.
-    rewrite int_iter_succ_l.
+    rewrite issemigrouppreserving_plus_abgroup_int_mult.
+    unfold abgroup_int_mult in *.
+    rewrite grp_pow_int_add_1.
     rhs nrapply rng_dist_r.
     rewrite rng_mult_one_l.
     rewrite IHx.
     reflexivity.
   - cbn.
     rewrite int_mul_pred_l.
-    rewrite issemigrouppreserving_plus_rng_int_mult.
     unfold rng_int_mult in *.
-    rewrite int_iter_pred_l.
+    rewrite issemigrouppreserving_plus_abgroup_int_mult.
+    unfold abgroup_int_mult in *.
+    rewrite grp_pow_int_sub_1.
     rhs nrapply rng_dist_r.
     rewrite IHx.
     f_ap.
-    lhs rapply rng_int_mult_neg.
+    lhs rapply abgroup_int_mult_neg.
     symmetry; apply rng_mult_negate.
 Defined.
 
@@ -107,8 +64,6 @@ Proof.
   1: exact (rng_int_mult R 1).
   repeat split.
   1,2: exact _.
-  hnf.
-  apply rng_plus_zero_r.
 Defined.
 
 (** The integers are the initial commutative ring *)
@@ -121,13 +76,15 @@ Proof.
   induction x as [|x|x].
   - by rhs nrapply (grp_homo_unit g).
   - unfold rng_homo_int, rng_int_mult; cbn.
-    rewrite int_iter_succ_l.
+    unfold abgroup_int_mult.
+    rewrite grp_pow_int_add_1.
     change (x.+1%int) with (1 + x)%int.
     rewrite (rng_homo_plus g 1 x).
     rewrite rng_homo_one.
     f_ap.
   - unfold rng_homo_int, rng_int_mult in IHx |- *; cbn in IHx |- *.
-    rewrite int_iter_pred_l.
+    unfold abgroup_int_mult in *.
+    rewrite grp_pow_int_sub_1.
     cbn.
     rewrite IHx.
     clear IHx.

From be2de281310b901a7210eb8a15bf630f26fde5ed Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Sun, 30 Jun 2024 15:43:01 +0200
Subject: [PATCH 10/14] remove comment about switching to int as this has been
 done

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Algebra/AbGroups/Z.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
index 727e72361e3..c1e23fdd868 100644
--- a/theories/Algebra/AbGroups/Z.v
+++ b/theories/Algebra/AbGroups/Z.v
@@ -10,7 +10,6 @@ Local Set Universe Minimization ToSet.
 
 Local Open Scope int_scope.
 
-(** TODO: switch to [Int] *)
 Definition abgroup_Z@{} : AbGroup@{Set}.
 Proof.
   snrapply Build_AbGroup.

From 1ba97c8be563606d33730c7ce3dcd530a3a51cf1 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Sun, 30 Jun 2024 16:27:05 -0400
Subject: [PATCH 11/14] Various cleanups to grp_pow, ab_mul, abgroup_int_mult
 and rng_int_mult

---
 theories/Algebra/AbGroups/AbelianGroup.v | 19 +++++++------
 theories/Algebra/AbGroups/Cyclic.v       |  2 +-
 theories/Algebra/AbGroups/Z.v            | 36 +++++++-----------------
 theories/Algebra/AbSES/SixTerm.v         |  2 +-
 theories/Algebra/Groups/Group.v          |  8 +++---
 theories/Algebra/Rings/Z.v               | 33 ++++++++--------------
 6 files changed, 38 insertions(+), 62 deletions(-)

diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v
index ff59e2b0219..1e0fc43e199 100644
--- a/theories/Algebra/AbGroups/AbelianGroup.v
+++ b/theories/Algebra/AbGroups/AbelianGroup.v
@@ -258,10 +258,11 @@ Proof.
       exact IHn.
 Defined.
 
-Definition ab_mul_homo {A B : AbGroup}
+(** [ab_mul n] is natural. *)
+Definition ab_mul_natural {A B : AbGroup}
   (f : GroupHomomorphism A B) (n : Int)
   : f o ab_mul n == ab_mul n o f
-  := grp_pow_homo f n.
+  := grp_pow_natural f n.
 
 (** The image of an inclusion is a normal subgroup. *)
 Definition ab_image_embedding {A B : AbGroup} (f : A $-> B) `{IsEmbedding f} : NormalSubgroup B
@@ -303,17 +304,17 @@ Proof.
 Defined.
 
 (** If the function is constant in the range of a finite sum then the sum is equal to the constant times [n]. This is a group power in the underlying group. *)
-Definition ab_sum_const {A : AbGroup} (n : nat) (r : A)
-  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = r)
-  : ab_sum n f = grp_pow r n.
+Definition ab_sum_const {A : AbGroup} (n : nat) (a : A)
+  (f : forall k, (k < n)%nat -> A) (p : forall k Hk, f k Hk = a)
+  : ab_sum n f = ab_mul n a.
 Proof.
   induction n as [|n IHn] in f, p |- *.
   - reflexivity.
-  - rewrite int_of_nat_succ_commute, grp_pow_int_add_1.
+  - rewrite int_of_nat_succ_commute.
+    rhs nrapply grp_pow_int_add_1.
     simpl. f_ap.
-    rewrite IHn.
-    + reflexivity.
-    + intros. apply p.
+    apply IHn.
+    intros. apply p.
 Defined.
 
 (** If the function is zero in the range of a finite sum then the sum is zero. *)
diff --git a/theories/Algebra/AbGroups/Cyclic.v b/theories/Algebra/AbGroups/Cyclic.v
index 7c658022c05..d8e00f31df6 100644
--- a/theories/Algebra/AbGroups/Cyclic.v
+++ b/theories/Algebra/AbGroups/Cyclic.v
@@ -48,7 +48,7 @@ Lemma Z1_mul_nat_beta {A : AbGroup} (a : A) (n : nat)
 Proof.
   induction n as [|n H].
   1: easy.
-  refine (grp_pow_homo _ _ _ @ _); simpl.
+  refine (grp_pow_natural _ _ _ @ _); simpl.
   by rewrite grp_unit_r.
 Defined.
 
diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
index c1e23fdd868..8247d2e3333 100644
--- a/theories/Algebra/AbGroups/Z.v
+++ b/theories/Algebra/AbGroups/Z.v
@@ -24,32 +24,16 @@ Defined.
 
 Local Open Scope mc_scope.
 
-(** Every element of an abelian group can be multiplied by an integer. *)
-Definition abgroup_int_mult (A : AbGroup) (x : A) (z : abgroup_Z) : A
-  := grp_pow x z.
-
-(** [abgroup_int_mult A r] preserves addition. *)
-Global Instance issemigrouppreserving_plus_abgroup_int_mult (A : AbGroup) (x : A)
-  : IsSemiGroupPreserving (Aop:=(+)) (Bop:=(+)) (abgroup_int_mult A x).
+(** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism. *)
+Definition grp_pow_homo {G : Group} (g : G)
+  : GroupHomomorphism abgroup_Z G.
 Proof.
-  intros y z.
-  apply grp_pow_int_add.
+  snrapply Build_GroupHomomorphism.
+  1: exact (grp_pow g).
+  intros m n; apply grp_pow_int_add.
 Defined.
 
-(** [abgroup_int_mult A r] sends [0 : Int] to [0 : R] definitionally. *)
-Global Instance isunitpreserving_plus_abgroup_int_mult (A : AbGroup) (x : A)
-  : IsUnitPreserving (Aunit:=zero) (Bunit:=canonical_names.zero)
-      (abgroup_int_mult A x)
-  := idpath.
-
-(** [abgroup_int_mult R r] preserves addition and zero. *)
-Global Instance ismonoidpreserving_plus_abgroup_int_mult (A : AbGroup) (x : A)
-  : IsMonoidPreserving (Aop:=(+)) (Bop:=(+)) (abgroup_int_mult A x)
-  := {}.
-
-(** [abgroup_int_mult R r] commutes with negation. *)
-Definition abgroup_int_mult_neg (A : AbGroup) (x : A) z
-  : abgroup_int_mult A x (- z) = - abgroup_int_mult A x z.
-Proof.
-  snrapply (groups.preserves_negate _); exact _.
-Defined.
+(** The special case for an abelian group, which gives multiplication by an integer. *)
+Definition abgroup_int_mult (A : AbGroup) (a : A)
+  : GroupHomomorphism abgroup_Z A
+  := grp_pow_homo a.
diff --git a/theories/Algebra/AbSES/SixTerm.v b/theories/Algebra/AbSES/SixTerm.v
index 6f07a6937f0..560effb9eae 100644
--- a/theories/Algebra/AbSES/SixTerm.v
+++ b/theories/Algebra/AbSES/SixTerm.v
@@ -211,7 +211,7 @@ Proof.
     apply moveR_equiv_V; symmetry.
     refine (ap f _ @ _).
     1: apply Z1_rec_beta.
-    exact (ab_mul_homo f n Z1_gen).
+    exact (ab_mul_natural f n Z1_gen).
   - (* we get rid of [equiv_Z1_hom] *)
     apply isexact_equiv_fiber.
     apply isexact_ext_cyclic_ab_iii.
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 1c5f643b672..4093c25ad80 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -476,7 +476,7 @@ End GroupMovement.
 
 (** ** Power operation *)
 
-(** For a given [n : nat] we can define the [n]th power of a group element. *)
+(** For a given [g : G] we can define the function [Int -> G] sending an integer to that power of [g]. *)
 Definition grp_pow {G : Group} (g : G) (n : Int) : G
   := match n with
      | posS n => nat_iter n (g *.) g
@@ -484,8 +484,8 @@ Definition grp_pow {G : Group} (g : G) (n : Int) : G
      | negS n => nat_iter n ((- g) *.) (- g)
      end.
 
-(** Any homomorphism respects [grp_pow]. *)
-Lemma grp_pow_homo {G H : Group} (f : GroupHomomorphism G H) (n : Int) (g : G)
+(** Any homomorphism respects [grp_pow]. In other words, [fun g => grp_pow g n] is natural. *)
+Lemma grp_pow_natural {G H : Group} (f : GroupHomomorphism G H) (n : Int) (g : G)
   : f (grp_pow g n) = grp_pow (f g) n.
 Proof.
   induction n.
@@ -559,7 +559,7 @@ Proof.
   - destruct n; simpl; rewrite grp_inv_inv; reflexivity.
 Defined.
 
-(** [grp_pow] satisfies a law of exponents. *)
+(** [grp_pow] satisfies an additive law of exponents. *)
 Definition grp_pow_int_add {G : Group} (m n : Int) (g : G)
   : grp_pow g (n + m)%int = grp_pow g n * grp_pow g m.
 Proof.
diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v
index cd22b4a5a89..ea1470e6b73 100644
--- a/theories/Algebra/Rings/Z.v
+++ b/theories/Algebra/Rings/Z.v
@@ -24,36 +24,31 @@ Defined.
 
 Local Open Scope mc_scope.
 
-Definition rng_int_mult (R : Ring) := abgroup_int_mult R. 
+(** Given a ring element [r], we get a map [Int -> R] sending an integer to that multiple of [r]. *)
+Definition rng_int_mult (R : Ring) := grp_pow_homo : R -> Int -> R.
 
 (** [rng_int_mult R 1] preserves multiplication.  This requires that the specified ring element is the unit. *)
 Global Instance issemigrouppreserving_mult_rng_int_mult (R : Ring)
   : IsSemiGroupPreserving (A:=cring_Z) (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R 1).
 Proof.
   intros x y.
+  cbn.
   induction x as [|x|x].
   - simpl.
     by rhs nrapply rng_mult_zero_l.
-  - cbn.
-    rewrite int_mul_succ_l.
-    unfold rng_int_mult in *.
-    rewrite issemigrouppreserving_plus_abgroup_int_mult.
-    unfold abgroup_int_mult in *.
+  - rewrite int_mul_succ_l.
+    rewrite grp_pow_int_add.
     rewrite grp_pow_int_add_1.
     rhs nrapply rng_dist_r.
     rewrite rng_mult_one_l.
-    rewrite IHx.
-    reflexivity.
-  - cbn.
-    rewrite int_mul_pred_l.
-    unfold rng_int_mult in *.
-    rewrite issemigrouppreserving_plus_abgroup_int_mult.
-    unfold abgroup_int_mult in *.
+    f_ap.
+  - rewrite int_mul_pred_l.
+    rewrite grp_pow_int_add.
     rewrite grp_pow_int_sub_1.
     rhs nrapply rng_dist_r.
     rewrite IHx.
     f_ap.
-    lhs rapply abgroup_int_mult_neg.
+    lhs rapply (grp_homo_inv (grp_pow_homo 1)).
     symmetry; apply rng_mult_negate.
 Defined.
 
@@ -73,19 +68,15 @@ Proof.
   intro R.
   exists (rng_homo_int R).
   intros g x.
+  unfold rng_homo_int, rng_int_mult; cbn.
   induction x as [|x|x].
   - by rhs nrapply (grp_homo_unit g).
-  - unfold rng_homo_int, rng_int_mult; cbn.
-    unfold abgroup_int_mult.
-    rewrite grp_pow_int_add_1.
+  - rewrite grp_pow_int_add_1.
     change (x.+1%int) with (1 + x)%int.
     rewrite (rng_homo_plus g 1 x).
     rewrite rng_homo_one.
     f_ap.
-  - unfold rng_homo_int, rng_int_mult in IHx |- *; cbn in IHx |- *.
-    unfold abgroup_int_mult in *.
-    rewrite grp_pow_int_sub_1.
-    cbn.
+  - rewrite grp_pow_int_sub_1.
     rewrite IHx.
     clear IHx.
     rewrite <- (rng_homo_one g).

From 0eb264368aa42bb824a7a9024c3be2c51616c242 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Tue, 2 Jul 2024 17:33:01 -0400
Subject: [PATCH 12/14] Algebra/*: Use int_iter for grp_pow

---
 theories/Algebra/AbGroups/AbelianGroup.v | 39 ++++++------
 theories/Algebra/Groups/Group.v          | 81 +++++++-----------------
 theories/Algebra/Rings/Z.v               |  3 +-
 theories/Spaces/Int.v                    | 16 +++++
 4 files changed, 59 insertions(+), 80 deletions(-)

diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v
index 21983e60b41..1d850ddd8fd 100644
--- a/theories/Algebra/AbGroups/AbelianGroup.v
+++ b/theories/Algebra/AbGroups/AbelianGroup.v
@@ -228,6 +228,20 @@ Proof.
     1-2: exact negate_involutive.
 Defined.
 
+(** This goal comes up twice in the proof of [ab_mul], so we factor it out. *)
+Local Definition ab_mul_helper {A : AbGroup} (a b x y z : A)
+  (p : x = y + z)
+  : a + b + x = a + y + (b + z).
+Proof.
+  lhs_V srapply grp_assoc.
+  rhs_V srapply grp_assoc.
+  apply grp_cancelL.
+  rhs srapply grp_assoc.
+  rhs nrapply (ap (fun g => g + z) (ab_comm y b)).
+  rhs_V srapply grp_assoc.
+  apply grp_cancelL, p.
+Defined.
+
 (** Multiplication by [n : Int] defines an endomorphism of any abelian group [A]. *)
 Definition ab_mul {A : AbGroup} (n : Int) : GroupHomomorphism A A.
 Proof.
@@ -236,26 +250,11 @@ Proof.
   intros a b.
   induction n; cbn.
   - exact (grp_unit_l _)^.
-  - destruct n.
-    + reflexivity.
-    + rhs_V srapply (associativity a).
-      rhs srapply (ap _ (associativity _ b _)).
-      rewrite (commutativity (nat_iter _ _ _) b).
-      rhs_V srapply (ap _ (associativity b _ _)).
-      rhs srapply (associativity a).
-      apply grp_cancelL.
-      exact IHn.
-  - destruct n.
-    + rewrite (commutativity (-a)).
-      exact (grp_inv_op a b).
-    + rhs_V srapply (associativity (-a)).
-      rhs srapply (ap _ (associativity _ (-b) _)).
-      rewrite (commutativity (nat_iter _ _ _) (-b)).
-      rhs_V srapply (ap _ (associativity (-b) _ _)).
-      rhs srapply (associativity (-a)).
-      rewrite (commutativity (-a) (-b)), <- (grp_inv_op a b).
-      apply grp_cancelL.
-      exact IHn.
+  - rewrite 3 grp_pow_int_add_1.
+    by apply ab_mul_helper.
+  - rewrite 3 grp_pow_int_sub_1.
+    rewrite (grp_inv_op a b), (commutativity (-b) (-a)).
+    by apply ab_mul_helper.
 Defined.
 
 (** [ab_mul n] is natural. *)
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 4093c25ad80..dcef27dbb68 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -478,98 +478,61 @@ End GroupMovement.
 
 (** For a given [g : G] we can define the function [Int -> G] sending an integer to that power of [g]. *)
 Definition grp_pow {G : Group} (g : G) (n : Int) : G
-  := match n with
-     | posS n => nat_iter n (g *.) g
-     | zero => mon_unit
-     | negS n => nat_iter n ((- g) *.) (- g)
-     end.
+  := int_iter (g *.) n mon_unit.
 
 (** Any homomorphism respects [grp_pow]. In other words, [fun g => grp_pow g n] is natural. *)
 Lemma grp_pow_natural {G H : Group} (f : GroupHomomorphism G H) (n : Int) (g : G)
   : f (grp_pow g n) = grp_pow (f g) n.
 Proof.
-  induction n.
-  - apply grp_homo_unit.
-  - destruct n; simpl in IHn |- *.
-    + reflexivity.
-    + lhs snrapply grp_homo_op.
-      apply ap.
-      exact IHn.
-  - destruct n; simpl in IHn |- *.
-    + apply grp_homo_inv.
-    + lhs snrapply grp_homo_op.
-      apply ap011.
-      * apply grp_homo_inv.
-      * exact IHn.
+  lhs snrapply (int_iter_commute_map _ ((f g) *.)).
+  1: nrapply grp_homo_op.
+  apply (ap (int_iter _ n)), grp_homo_unit.
 Defined.
 
 (** All powers of the unit are the unit. *)
 Definition grp_pow_unit {G : Group} (n : Int)
   : grp_pow (G:=G) mon_unit n = mon_unit.
 Proof.
-  induction n.
+  snrapply (int_iter_invariant n _ (fun g => g = mon_unit)); cbn.
+  1, 2: apply paths_ind_r.
+  - apply grp_unit_r.
+  - lhs nrapply grp_unit_r. apply grp_inv_unit.
   - reflexivity.
-  - destruct n; simpl. 
-    + reflexivity.
-    + by lhs nrapply grp_unit_l.
-  - destruct n; simpl in IHn |- *.
-    + apply grp_inv_unit.
-    + destruct IHn^.
-      rhs_V apply (@grp_inv_unit G).
-      apply grp_unit_r.
 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. *)
 
-(** Helper functions for [grp_pow_int_add]. This is how we can unfold [grp_pow] once. *)
-
+(** The next two results tell us how [grp_pow] unfolds. *)
 Definition grp_pow_int_add_1 {G : Group} (n : Int) (g : G)
-  : grp_pow g (n.+1)%int = g * grp_pow g n.
-Proof.
-  induction n; simpl.
-  - exact (grp_unit_r g)^.
-  - destruct n; reflexivity.
-  - destruct n.
-    + apply (grp_inv_r g)^.
-    + rhs srapply associativity.
-      rewrite grp_inv_r. 
-      apply (grp_unit_l _)^.
-Defined.
+  : 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)
-  : grp_pow g (n.-1)%int = (- g) * grp_pow g n.
-Proof.
-  induction n; simpl.
-  - exact (grp_unit_r (-g))^.
-  - destruct n.
-    + apply (grp_inv_l g)^.
-    + rhs srapply associativity.
-      rewrite grp_inv_l.
-      apply (grp_unit_l _)^.
-  - destruct n; reflexivity.
-Defined.
+  : 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.
-  induction n.
+  lhs nrapply int_iter_neg.
+  destruct n.
+  - cbn. by rewrite grp_inv_inv.
+  - reflexivity.
   - reflexivity.
-  - destruct n; reflexivity.
-  - destruct n; simpl; rewrite grp_inv_inv; reflexivity.
 Defined.
 
 (** [grp_pow] satisfies an additive law of exponents. *)
 Definition grp_pow_int_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_add_succ_l, 2 grp_pow_int_add_1.
-  2: rewrite int_add_pred_l, 2 grp_pow_int_sub_1.
-  1,2: rhs_V srapply associativity; 
-       snrapply (ap (_ *.));
-       exact IHn.
+  1: rewrite int_iter_succ_l, grp_pow_int_add_1.
+  2: rewrite int_iter_pred_l, grp_pow_int_sub_1; cbn.
+  1,2 : rhs_V srapply associativity;
+        apply ap, IHn.
 Defined.
 
 (** ** The category of Groups *)
diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v
index ea1470e6b73..cfe74590276 100644
--- a/theories/Algebra/Rings/Z.v
+++ b/theories/Algebra/Rings/Z.v
@@ -32,7 +32,7 @@ Global Instance issemigrouppreserving_mult_rng_int_mult (R : Ring)
   : IsSemiGroupPreserving (A:=cring_Z) (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R 1).
 Proof.
   intros x y.
-  cbn.
+  cbn; unfold sg_op.
   induction x as [|x|x].
   - simpl.
     by rhs nrapply rng_mult_zero_l.
@@ -59,6 +59,7 @@ Proof.
   1: exact (rng_int_mult R 1).
   repeat split.
   1,2: exact _.
+  apply rng_plus_zero_r.
 Defined.
 
 (** The integers are the initial commutative ring *)
diff --git a/theories/Spaces/Int.v b/theories/Spaces/Int.v
index 6b4a8130b99..da60ce1c189 100644
--- a/theories/Spaces/Int.v
+++ b/theories/Spaces/Int.v
@@ -634,6 +634,22 @@ Proof.
     apply eisretr.
 Defined.
 
+Definition int_iter_invariant (n : Int) {A} (f : A -> A) `{!IsEquiv f}
+  (P : A -> Type)
+  (Psucc : forall x, P x -> P (f x))
+  (Ppred : forall x, P x -> P (f^-1 x))
+  : forall x, P x -> P (int_iter f n x).
+Proof.
+  induction n as [|n IHn|n IHn]; intro x.
+  - exact idmap.
+  - intro H.
+    rewrite int_iter_succ_l.
+    apply Psucc, IHn, H.
+  - intro H.
+    rewrite int_iter_pred_l.
+    apply Ppred, IHn, H.
+Defined.
+
 (** ** Exponentiation of loops *)
 
 Definition loopexp {A : Type} {x : A} (p : x = x) (z : Int) : (x = x)

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 13/14] 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).

From 1e60610195e93afcfb05bad697573d36a737586f Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 3 Jul 2024 08:37:34 -0400
Subject: [PATCH 14/14] AbGroups/Z: get rid of abgroup_int_mult

---
 theories/Algebra/AbGroups/Z.v | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v
index 1dcde9e0927..d476119a3f1 100644
--- a/theories/Algebra/AbGroups/Z.v
+++ b/theories/Algebra/AbGroups/Z.v
@@ -22,8 +22,6 @@ Proof.
   - exact int_add_comm.
 Defined.
 
-Local Open Scope mc_scope.
-
 (** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism. *)
 Definition grp_pow_homo {G : Group} (g : G)
   : GroupHomomorphism abgroup_Z G.
@@ -32,8 +30,3 @@ Proof.
   1: exact (grp_pow g).
   intros m n; apply grp_pow_add.
 Defined.
-
-(** The special case for an abelian group, which gives multiplication by an integer. *)
-Definition abgroup_int_mult (A : AbGroup) (a : A)
-  : GroupHomomorphism abgroup_Z A
-  := grp_pow_homo a.