Require Import Classes.interfaces.canonical_names.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import Algebra.AbGroups.
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. *)

(** The ring of integers *)
Definition cring_Z : CRing.
CRing
Proof.
CRing
  snrapply Build_CRing'.
AbGroup
One ?R
Mult ?R
Commutative mult
LeftDistribute mult plus
IsMonoid ?R
  -
AbGroup exact abgroup_Z.
  -
One abgroup_Z exact 1%int.
  -
Mult abgroup_Z exact int_mul.
  -
Commutative mult exact int_mul_comm.
  -
LeftDistribute mult plus exact int_mul_add_distr_l.
  -
IsMonoid abgroup_Z split.
IsSemiGroup abgroup_Z
LeftIdentity sg_op mon_unit
RightIdentity sg_op mon_unit
    +
IsSemiGroup abgroup_Z split.
IsHSet abgroup_Z
Associative sg_op
      *
IsHSet abgroup_Z exact _.
      *
Associative sg_op exact int_mul_assoc.
    +
LeftIdentity sg_op mon_unit exact int_mul_1_l.
    +
RightIdentity sg_op mon_unit 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%int => 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).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
forall x : G, IsEquiv (fun t : G => sg_op x t)
Proof.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
forall x : G, IsEquiv (fun t : G => sg_op x t)
  intro x.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
IsEquiv (fun t : G => sg_op x t)
  srapply isequiv_adjointify.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
G -> G
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
(fun t : G => sg_op x t) o ?g == idmap
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
?g o (fun t : G => sg_op x t) == idmap
  1: exact (sg_op (-x)).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
(fun t : G => sg_op x t) o sg_op (- x) == idmap
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
sg_op (- x) o (fun t : G => sg_op x t) == idmap
  all: intro y.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op x (sg_op (- x) y) = y
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op (- x) (sg_op x y) = y
  all: refine (associativity _ _ _ @ _ @ left_identity y).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op (sg_op x (- x)) y = sg_op mon_unit y
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op (sg_op (- x) x) y = sg_op mon_unit y
  all: refine (ap (fun x => x * y) _).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op x (- x) = mon_unit
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op (- x) x = mon_unit
  1: apply right_inverse.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op (- x) x = mon_unit
  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).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
forall x : G, IsEquiv (fun y : G => sg_op y x)
Proof.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
forall x : G, IsEquiv (fun y : G => sg_op y x)
  intro x.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
IsEquiv (fun y : G => sg_op y x)
  srapply isequiv_adjointify.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
G -> G
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
(fun y : G => sg_op y x) o ?g == idmap
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
?g o (fun y : G => sg_op y x) == idmap
  1: exact (fun y => sg_op y (- x)).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
(fun y : G => sg_op y x)
o (fun y : G => sg_op y (- x)) == idmap
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x: G
(fun y : G => sg_op y (- x))
o (fun y : G => sg_op y x) == idmap
  all: intro y.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op (sg_op y (- x)) x = y
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op (sg_op y x) (- x) = y
  all: refine ((associativity _ _ _)^ @ _ @ right_identity y).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op y (sg_op (- x) x) = sg_op y mon_unit
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op y (sg_op x (- x)) = sg_op y mon_unit
  all: refine (ap (y *.) _).
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op (- x) x = mon_unit
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op x (- x) = mon_unit
  1: apply left_inverse.
G: Type
Aop: SgOp G
Aunit: MonUnit G
Anegate: Negate G
H: IsGroup G
x, y: G
sg_op x (- x) = mon_unit
  apply right_inverse.
Defined.

(** 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).
R: CRing
IsSemiGroupPreserving
  (cring_catamorphism_fun R : cring_Z -> R)
Proof.
R: CRing
IsSemiGroupPreserving
  (cring_catamorphism_fun R : cring_Z -> R)
  (** Unfortunately, due to how we have defined things we need to seperate this out into 9 cases. *)
  hnf.
R: CRing
forall x y : cring_Z,
cring_catamorphism_fun R (sg_op x y) =
sg_op (cring_catamorphism_fun R x)
  (cring_catamorphism_fun R y) intros [x| |x] [y| |y].
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (neg y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x: Pos
cring_catamorphism_fun R (sg_op (neg x) 0%int) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R 0%int)
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (pos y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (pos y))
R: CRing
y: Pos
cring_catamorphism_fun R (sg_op 0%int (neg y)) =
sg_op (cring_catamorphism_fun R 0%int)
  (cring_catamorphism_fun R (neg y))
R: CRing
cring_catamorphism_fun R (sg_op 0%int 0%int) =
sg_op (cring_catamorphism_fun R 0%int)
  (cring_catamorphism_fun R 0%int)
R: CRing
y: Pos
cring_catamorphism_fun R (sg_op 0%int (pos y)) =
sg_op (cring_catamorphism_fun R 0%int)
  (cring_catamorphism_fun R (pos y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x: Pos
cring_catamorphism_fun R (sg_op (pos x) 0%int) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R 0%int)
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y))
  (** Some of these cases are easy however *)
  2,5,8: cbn; by rewrite right_identity.
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (neg y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (pos y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (pos y))
R: CRing
y: Pos
cring_catamorphism_fun R (sg_op 0%int (neg y)) =
sg_op (cring_catamorphism_fun R 0%int)
  (cring_catamorphism_fun R (neg y))
R: CRing
y: Pos
cring_catamorphism_fun R (sg_op 0%int (pos y)) =
sg_op (cring_catamorphism_fun R 0%int)
  (cring_catamorphism_fun R (pos y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y))
  3,4: symmetry; apply left_identity.
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (neg y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (pos y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (pos y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y))
  (** This leaves us with four cases to consider *)
  (** x < 0 , y < 0 *)
  {
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (neg y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (neg y)) change (cring_catamorphism_fun R ((neg x) + (neg y))%int
      = (cring_catamorphism_fun R (neg x)) + (cring_catamorphism_fun R (neg y))).
R: CRing
x, y: Pos
cring_catamorphism_fun R (neg x + neg y)%int =
cring_catamorphism_fun R (neg x) +
cring_catamorphism_fun R (neg y)
    induction y as [|y IHy] using pos_peano_ind.
R: CRing
x: Pos
cring_catamorphism_fun R (neg x + -1)%int =
cring_catamorphism_fun R (neg x) +
cring_catamorphism_fun R (-1)%int
R: CRing
x, y: Pos
IHy: cring_catamorphism_fun R (neg x + neg y)%int =
cring_catamorphism_fun R (neg x) + cring_catamorphism_fun R (neg y)
cring_catamorphism_fun R
  (neg x + neg (pos_succ y))%int =
cring_catamorphism_fun R (neg x) +
cring_catamorphism_fun R (neg (pos_succ y))
    {
R: CRing
x: Pos
cring_catamorphism_fun R (neg x + -1)%int =
cring_catamorphism_fun R (neg x) +
cring_catamorphism_fun R (-1)%int simpl.
R: CRing
x: Pos
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) (x + 1)%pos =
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos
      rewrite pos_add_1_r.
R: CRing
x: Pos
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ x) =
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos
      rewrite pos_peano_rec_beta_pos_succ.
R: CRing
x: Pos
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x =
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos
      apply commutativity. }
R: CRing
x, y: Pos
IHy: cring_catamorphism_fun R (neg x + neg y)%int =
cring_catamorphism_fun R (neg x) + cring_catamorphism_fun R (neg y)
cring_catamorphism_fun R
  (neg x + neg (pos_succ y))%int =
cring_catamorphism_fun R (neg x) +
cring_catamorphism_fun R (neg (pos_succ y))
    simpl.
R: CRing
x, y: Pos
IHy: cring_catamorphism_fun R (neg x + neg y)%int =
cring_catamorphism_fun R (neg x) + cring_catamorphism_fun R (neg y)
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr)
  (x + pos_succ y)%pos =
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y)
    rewrite pos_add_succ_r.
R: CRing
x, y: Pos
IHy: cring_catamorphism_fun R (neg x + neg y)%int =
cring_catamorphism_fun R (neg x) + cring_catamorphism_fun R (neg y)
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr)
  (pos_succ (x + y)%pos) =
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y)
    rewrite 2 pos_peano_rec_beta_pos_succ.
R: CRing
x, y: Pos
IHy: cring_catamorphism_fun R (neg x + neg y)%int =
cring_catamorphism_fun R (neg x) + cring_catamorphism_fun R (neg y)
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) (x + y)%pos =
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x +
(-1 +
 pos_peano_rec R (-1)
   (fun (_ : Pos) (nr : R) => -1 + nr) y)
    rewrite simple_associativity.
R: CRing
x, y: Pos
IHy: cring_catamorphism_fun R (neg x + neg y)%int =
cring_catamorphism_fun R (neg x) + cring_catamorphism_fun R (neg y)
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) (x + y)%pos =
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x - 1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) y
    rewrite (commutativity _ (-1)).
R: CRing
x, y: Pos
IHy: cring_catamorphism_fun R (neg x + neg y)%int =
cring_catamorphism_fun R (neg x) + cring_catamorphism_fun R (neg y)
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) (x + y)%pos =
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) y
    rewrite <- simple_associativity.
R: CRing
x, y: Pos
IHy: cring_catamorphism_fun R (neg x + neg y)%int =
cring_catamorphism_fun R (neg x) + cring_catamorphism_fun R (neg y)
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) (x + y)%pos =
-1 +
(pos_peano_rec R (-1)
   (fun (_ : Pos) (nr : R) => -1 + nr) x +
 pos_peano_rec R (-1)
   (fun (_ : Pos) (nr : R) => -1 + nr) y)
    f_ap. }
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (pos y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (pos y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y))
  (** x < 0 , y > 0 *)
  {
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (pos y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (pos y)) cbn.
R: CRing
x, y: Pos
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    revert x.
R: CRing
y: Pos
forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    induction y as [|y IHy] using pos_peano_ind; intro x.
R: CRing
x: Pos
cring_catamorphism_fun R (int_pos_sub 1%pos x) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) 1%pos)
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
    {
R: CRing
x: Pos
cring_catamorphism_fun R (int_pos_sub 1%pos x) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) 1%pos) cbn.
R: CRing
x: Pos
cring_catamorphism_fun R (int_pos_sub 1%pos x) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x) 1
      induction x as [|x] using pos_peano_ind.
R: CRing
cring_catamorphism_fun R (int_pos_sub 1%pos 1%pos) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos) 1
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub 1%pos x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x) 1
cring_catamorphism_fun R
  (int_pos_sub 1%pos (pos_succ x)) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ x))
  1
      1: symmetry; cbn; apply left_inverse.
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub 1%pos x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x) 1
cring_catamorphism_fun R
  (int_pos_sub 1%pos (pos_succ x)) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ x))
  1
      rewrite pos_peano_rec_beta_pos_succ.
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub 1%pos x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x) 1
cring_catamorphism_fun R
  (int_pos_sub 1%pos (pos_succ x)) =
sg_op
  (-1 +
   pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x) 1
      rewrite int_pos_sub_succ_r.
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub 1%pos x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x) 1
cring_catamorphism_fun R (neg x) =
sg_op
  (-1 +
   pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x) 1
      cbn; rewrite <- simple_associativity.
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub 1%pos x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x) 1
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x =
sg_op (-1)
  (sg_op
     (pos_peano_rec R (-1)
        (fun (_ : Pos) (nr : R) => -1 + nr) x) 1)
      apply (rng_moveL_Vr (R:=R)).
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub 1%pos x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x) 1
1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x) 1
      apply commutativity. }
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
    induction x as [|x IHx] using pos_peano_ind.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
cring_catamorphism_fun R
  (int_pos_sub (pos_succ y) 1%pos) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
cring_catamorphism_fun R
  (int_pos_sub (pos_succ y) (pos_succ x)) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ x))
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
    {
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
cring_catamorphism_fun R
  (int_pos_sub (pos_succ y) 1%pos) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y)) rewrite int_pos_sub_succ_l.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
cring_catamorphism_fun R (pos y) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
      cbn; apply (rng_moveL_Vr (R:=R)).
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y =
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (pos_succ y)
      by rewrite pos_peano_rec_beta_pos_succ. }
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
cring_catamorphism_fun R
  (int_pos_sub (pos_succ y) (pos_succ x)) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ x))
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
    rewrite int_pos_sub_succ_succ.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ x))
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
    rewrite IHy.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ x))
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
    rewrite 2 pos_peano_rec_beta_pos_succ.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y) =
sg_op
  (-1 +
   pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (1 +
   pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    rewrite (commutativity (-1)).
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y) =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x - 1)
  (1 +
   pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    rewrite simple_associativity.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y) =
sg_op
  (sg_op
     (pos_peano_rec R (-1)
        (fun (_ : Pos) (nr : R) => -1 + nr) x - 1) 1)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    rewrite <- (simple_associativity _ _ 1).
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y) =
sg_op
  (sg_op
     (pos_peano_rec R (-1)
        (fun (_ : Pos) (nr : R) => -1 + nr) x)
     (sg_op (-1) 1))
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    rewrite left_inverse.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y) =
sg_op
  (sg_op
     (pos_peano_rec R (-1)
        (fun (_ : Pos) (nr : R) => -1 + nr) x)
     mon_unit)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    f_ap.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x =
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x) mon_unit
    symmetry.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub y x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub (pos_succ y) x) =
sg_op (pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) x) mon_unit =
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) x
    apply right_identity. }
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y))
  -
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y)) cbn.
R: CRing
x, y: Pos
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y)
    revert x.
R: CRing
y: Pos
forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y)
    induction y as [|y IHy] using pos_peano_ind; intro x.
R: CRing
x: Pos
cring_catamorphism_fun R (int_pos_sub x 1%pos) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
    {
R: CRing
x: Pos
cring_catamorphism_fun R (int_pos_sub x 1%pos) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos) induction x as [|x] using pos_peano_ind.
R: CRing
cring_catamorphism_fun R (int_pos_sub 1%pos 1%pos) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) 1%pos)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x 1%pos) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
cring_catamorphism_fun R
  (int_pos_sub (pos_succ x) 1%pos) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ x))
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
      1: symmetry; cbn; apply right_inverse.
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x 1%pos) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
cring_catamorphism_fun R
  (int_pos_sub (pos_succ x) 1%pos) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ x))
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
      rewrite pos_peano_rec_beta_pos_succ.
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x 1%pos) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
cring_catamorphism_fun R
  (int_pos_sub (pos_succ x) 1%pos) =
sg_op
  (1 +
   pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
      rewrite (commutativity 1).
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x 1%pos) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
cring_catamorphism_fun R
  (int_pos_sub (pos_succ x) 1%pos) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x + 1)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
      rewrite <- simple_associativity.
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x 1%pos) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
cring_catamorphism_fun R
  (int_pos_sub (pos_succ x) 1%pos) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (sg_op 1
     (pos_peano_rec R (-1)
        (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos))
      rewrite int_pos_sub_succ_l.
R: CRing
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x 1%pos) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos)
cring_catamorphism_fun R (pos x) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (sg_op 1
     (pos_peano_rec R (-1)
        (fun (_ : Pos) (nr : R) => -1 + nr) 1%pos))
      cbn; by rewrite right_inverse, right_identity. }
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
    induction x as [|x IHx] using pos_peano_ind.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
cring_catamorphism_fun R
  (int_pos_sub 1%pos (pos_succ y)) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) 1%pos)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
cring_catamorphism_fun R
  (int_pos_sub (pos_succ x) (pos_succ y)) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ x))
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
    {
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
cring_catamorphism_fun R
  (int_pos_sub 1%pos (pos_succ y)) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) 1%pos)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y)) rewrite int_pos_sub_succ_r.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
cring_catamorphism_fun R (neg y) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) 1%pos)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
      rewrite pos_peano_rec_beta_pos_succ.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
cring_catamorphism_fun R (neg y) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) 1%pos)
  (-1 +
   pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y)
      rewrite simple_associativity.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
cring_catamorphism_fun R (neg y) =
sg_op
  (sg_op
     (pos_peano_rec R 1
        (fun (_ : Pos) (nr : R) => 1 + nr) 1%pos) 
     (-1))
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y)
      cbn.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) y =
sg_op (sg_op 1 (-1))
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y)
      rewrite (right_inverse 1).
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) y =
sg_op mon_unit
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y)
      symmetry.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
sg_op mon_unit
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y) =
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) y
      apply left_identity. }
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
cring_catamorphism_fun R
  (int_pos_sub (pos_succ x) (pos_succ y)) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ x))
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
    rewrite int_pos_sub_succ_succ.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ x))
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
    rewrite IHy.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ x))
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
    rewrite 2 pos_peano_rec_beta_pos_succ.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y) =
sg_op
  (1 +
   pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (-1 +
   pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y)
    rewrite (commutativity 1).
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x + 1)
  (-1 +
   pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y)
    rewrite simple_associativity.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y) =
sg_op
  (sg_op
     (pos_peano_rec R 1
        (fun (_ : Pos) (nr : R) => 1 + nr) x + 1) 
     (-1))
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y)
    rewrite <- (simple_associativity _ _ (-1)).
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y) =
sg_op
  (sg_op
     (pos_peano_rec R 1
        (fun (_ : Pos) (nr : R) => 1 + nr) x)
     (sg_op 1 (-1)))
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y)
    rewrite (right_inverse 1).
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y) =
sg_op
  (sg_op
     (pos_peano_rec R 1
        (fun (_ : Pos) (nr : R) => 1 + nr) x) mon_unit)
  (pos_peano_rec R (-1)
     (fun (_ : Pos) (nr : R) => -1 + nr) y)
    f_ap; symmetry.
R: CRing
y: Pos
IHy: forall x : Pos,
cring_catamorphism_fun R (int_pos_sub x y) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) y)
x: Pos
IHx: cring_catamorphism_fun R (int_pos_sub x (pos_succ y)) =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R (-1) (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ y))
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x) mon_unit =
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x
    apply right_identity.
  -
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y)) cbn.
R: CRing
x, y: Pos
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (x + y)%pos =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    induction y as [|y IHy] using pos_peano_ind.
R: CRing
x: Pos
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (x + 1)%pos =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) 1%pos)
R: CRing
x, y: Pos
IHy: pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (x + y)%pos =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (x + pos_succ y)%pos =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
    {
R: CRing
x: Pos
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (x + 1)%pos =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) 1%pos) cbn.
R: CRing
x: Pos
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (x + 1)%pos =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x) 1
      rewrite pos_add_1_r.
R: CRing
x: Pos
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (pos_succ x) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x) 1
      rewrite pos_peano_rec_beta_pos_succ.
R: CRing
x: Pos
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x) 1
      apply commutativity. }
R: CRing
x, y: Pos
IHy: pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (x + y)%pos =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (x + pos_succ y)%pos =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
    rewrite pos_add_succ_r.
R: CRing
x, y: Pos
IHy: pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (x + y)%pos =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (pos_succ (x + y)%pos) =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) (pos_succ y))
    rewrite 2 pos_peano_rec_beta_pos_succ.
R: CRing
x, y: Pos
IHy: pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (x + y)%pos =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (x + y)%pos =
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (1 +
   pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    rewrite simple_associativity.
R: CRing
x, y: Pos
IHy: pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (x + y)%pos =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (x + y)%pos =
sg_op
  (sg_op
     (pos_peano_rec R 1
        (fun (_ : Pos) (nr : R) => 1 + nr) x) 1)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    rewrite IHy.
R: CRing
x, y: Pos
IHy: pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (x + y)%pos =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
1 +
sg_op
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) x)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y) =
sg_op
  (sg_op
     (pos_peano_rec R 1
        (fun (_ : Pos) (nr : R) => 1 + nr) x) 1)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    rewrite simple_associativity.
R: CRing
x, y: Pos
IHy: pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (x + y)%pos =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y =
sg_op
  (sg_op
     (pos_peano_rec R 1
        (fun (_ : Pos) (nr : R) => 1 + nr) x) 1)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    rewrite (commutativity 1).
R: CRing
x, y: Pos
IHy: pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) (x + y)%pos =
sg_op (pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x)
(pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y)
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) x +
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) y =
sg_op
  (sg_op
     (pos_peano_rec R 1
        (fun (_ : Pos) (nr : R) => 1 + nr) x) 1)
  (pos_peano_rec R 1
     (fun (_ : Pos) (nr : R) => 1 + nr) y)
    reflexivity.
Qed.

Lemma cring_catamorphism_fun_negate {R} x
  : cring_catamorphism_fun R (- x) = - cring_catamorphism_fun R x.
R: CRing
x: cring_Z
cring_catamorphism_fun R (- x) =
- cring_catamorphism_fun R x
Proof.
R: CRing
x: cring_Z
cring_catamorphism_fun R (- x) =
- cring_catamorphism_fun R x
  snrapply (groups.preserves_negate _).
R: CRing
x: cring_Z
SgOp cring_Z
R: CRing
x: cring_Z
MonUnit cring_Z
R: CRing
x: cring_Z
IsGroup cring_Z
R: CRing
x: cring_Z
SgOp R
R: CRing
x: cring_Z
MonUnit R
R: CRing
x: cring_Z
IsGroup R
R: CRing
x: cring_Z
IsMonoidPreserving (cring_catamorphism_fun R)
  1-6: typeclasses eauto.
R: CRing
x: cring_Z
IsMonoidPreserving (cring_catamorphism_fun R)
  snrapply Build_IsMonoidPreserving.
R: CRing
x: cring_Z
IsSemiGroupPreserving (cring_catamorphism_fun R)
R: CRing
x: cring_Z
IsUnitPreserving (cring_catamorphism_fun R)
  1: exact _.
R: CRing
x: cring_Z
IsUnitPreserving (cring_catamorphism_fun R)
  split.
Defined.

Lemma cring_catamorphism_fun_pos_mult {R} x y
  : cring_catamorphism_fun R (pos x * pos y)%int
    = cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y).
R: CRing
x, y: Pos
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) *
cring_catamorphism_fun R (pos y)
Proof.
R: CRing
x, y: Pos
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) *
cring_catamorphism_fun R (pos y)
  revert y.
R: CRing
x: Pos
forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) *
cring_catamorphism_fun R (pos y)
  induction x as [|x IHx] using pos_peano_ind; intro y.
R: CRing
y: Pos
cring_catamorphism_fun R (1 * pos y)%int =
cring_catamorphism_fun R 1%int *
cring_catamorphism_fun R (pos y)
R: CRing
x: Pos
IHx: forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y)
y: Pos
cring_catamorphism_fun R
  (pos (pos_succ x) * pos y)%int =
cring_catamorphism_fun R (pos (pos_succ x)) *
cring_catamorphism_fun R (pos y)
  {
R: CRing
y: Pos
cring_catamorphism_fun R (1 * pos y)%int =
cring_catamorphism_fun R 1%int *
cring_catamorphism_fun R (pos y) symmetry.
R: CRing
y: Pos
cring_catamorphism_fun R 1%int *
cring_catamorphism_fun R (pos y) =
cring_catamorphism_fun R (1 * pos y)%int
    apply left_identity. }
R: CRing
x: Pos
IHx: forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y)
y: Pos
cring_catamorphism_fun R
  (pos (pos_succ x) * pos y)%int =
cring_catamorphism_fun R (pos (pos_succ x)) *
cring_catamorphism_fun R (pos y)
  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)).
R: CRing
x: Pos
IHx: forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y)
y: Pos
cring_catamorphism_fun R (pos (pos_succ x * y)) =
cring_catamorphism_fun R (pos (pos_succ x)) *
cring_catamorphism_fun R (pos y)
  rewrite pos_mul_succ_l.
R: CRing
x: Pos
IHx: forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y)
y: Pos
cring_catamorphism_fun R (pos ((x * y)%pos + y)) =
cring_catamorphism_fun R (pos (pos_succ x)) *
cring_catamorphism_fun R (pos y)
  refine (issemigrouppreserving_cring_catamorphism_fun_plus
    R (pos (x * y)%pos) (pos y) @ _).
R: CRing
x: Pos
IHx: forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y)
y: Pos
sg_op (cring_catamorphism_fun R (pos (x * y)))
  (cring_catamorphism_fun R (pos y)) =
cring_catamorphism_fun R (pos (pos_succ x)) *
cring_catamorphism_fun R (pos y)
  rewrite IHx.
R: CRing
x: Pos
IHx: forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y)
y: Pos
sg_op
  (cring_catamorphism_fun R (pos x) *
   cring_catamorphism_fun R (pos y))
  (cring_catamorphism_fun R (pos y)) =
cring_catamorphism_fun R (pos (pos_succ x)) *
cring_catamorphism_fun R (pos y)
  transitivity ((1 + cring_catamorphism_fun R (pos x)) * cring_catamorphism_fun R (pos y)).
R: CRing
x: Pos
IHx: forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y)
y: Pos
sg_op
  (cring_catamorphism_fun R (pos x) *
   cring_catamorphism_fun R (pos y))
  (cring_catamorphism_fun R (pos y)) =
(1 + cring_catamorphism_fun R (pos x)) *
cring_catamorphism_fun R (pos y)
R: CRing
x: Pos
IHx: forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y)
y: Pos
(1 + cring_catamorphism_fun R (pos x)) *
cring_catamorphism_fun R (pos y) =
cring_catamorphism_fun R (pos (pos_succ x)) *
cring_catamorphism_fun R (pos y)
  2: simpl; by rewrite pos_peano_rec_beta_pos_succ.
R: CRing
x: Pos
IHx: forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y)
y: Pos
sg_op
  (cring_catamorphism_fun R (pos x) *
   cring_catamorphism_fun R (pos y))
  (cring_catamorphism_fun R (pos y)) =
(1 + cring_catamorphism_fun R (pos x)) *
cring_catamorphism_fun R (pos y)
  rewrite (rng_dist_r (A:=R)).
R: CRing
x: Pos
IHx: forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y)
y: Pos
sg_op
  (cring_catamorphism_fun R (pos x) *
   cring_catamorphism_fun R (pos y))
  (cring_catamorphism_fun R (pos y)) =
1 * cring_catamorphism_fun R (pos y) +
cring_catamorphism_fun R (pos x) *
cring_catamorphism_fun R (pos y)
  rewrite rng_mult_one_l.
R: CRing
x: Pos
IHx: forall y : Pos,
cring_catamorphism_fun R (pos x * pos y)%int =
cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y)
y: Pos
sg_op
  (cring_catamorphism_fun R (pos x) *
   cring_catamorphism_fun R (pos y))
  (cring_catamorphism_fun R (pos y)) =
cring_catamorphism_fun R (pos y) +
cring_catamorphism_fun R (pos x) *
cring_catamorphism_fun R (pos y)
  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).
R: CRing
IsSemiGroupPreserving
  (cring_catamorphism_fun R : cring_Z -> R)
Proof.
R: CRing
IsSemiGroupPreserving
  (cring_catamorphism_fun R : cring_Z -> R)
  hnf.
R: CRing
forall x y : cring_Z,
cring_catamorphism_fun R (sg_op x y) =
sg_op (cring_catamorphism_fun R x)
  (cring_catamorphism_fun R y) intros [x| |x] [y| |y].
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (neg y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x: Pos
cring_catamorphism_fun R (sg_op (neg x) 0%int) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R 0%int)
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (pos y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (pos y))
R: CRing
y: Pos
cring_catamorphism_fun R (sg_op 0%int (neg y)) =
sg_op (cring_catamorphism_fun R 0%int)
  (cring_catamorphism_fun R (neg y))
R: CRing
cring_catamorphism_fun R (sg_op 0%int 0%int) =
sg_op (cring_catamorphism_fun R 0%int)
  (cring_catamorphism_fun R 0%int)
R: CRing
y: Pos
cring_catamorphism_fun R (sg_op 0%int (pos y)) =
sg_op (cring_catamorphism_fun R 0%int)
  (cring_catamorphism_fun R (pos y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x: Pos
cring_catamorphism_fun R (sg_op (pos x) 0%int) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R 0%int)
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y))
  2,5,8: symmetry; apply (rng_mult_zero_r (A:=R)).
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (neg y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (pos y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (pos y))
R: CRing
y: Pos
cring_catamorphism_fun R (sg_op 0%int (neg y)) =
sg_op (cring_catamorphism_fun R 0%int)
  (cring_catamorphism_fun R (neg y))
R: CRing
y: Pos
cring_catamorphism_fun R (sg_op 0%int (pos y)) =
sg_op (cring_catamorphism_fun R 0%int)
  (cring_catamorphism_fun R (pos y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y))
  3,4: cbn; symmetry; rewrite (commutativity 0); apply (rng_mult_zero_r (A:=R)).
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (neg y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (pos y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (pos y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y))
  {
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (neg y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (neg y)) 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))).
R: CRing
x, y: Pos
cring_catamorphism_fun R (pos (x * y)) =
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)). }
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (pos y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (pos y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y))
  {
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (neg x) (pos y)) =
sg_op (cring_catamorphism_fun R (neg x))
  (cring_catamorphism_fun R (pos y)) 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)).
R: CRing
x, y: Pos
cring_catamorphism_fun R (- (pos (x * y) : 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)). }
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y))
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y))
  {
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (neg y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (neg y)) 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))).
R: CRing
x, y: Pos
cring_catamorphism_fun R (- (pos (x * y) : 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)). }
R: CRing
x, y: Pos
cring_catamorphism_fun R (sg_op (pos x) (pos y)) =
sg_op (cring_catamorphism_fun R (pos x))
  (cring_catamorphism_fun R (pos y))
  apply cring_catamorphism_fun_pos_mult.
Qed.

(** This is a ring homomorphism *)
Definition rng_homo_int (R : CRing) : cring_Z $-> R.
R: CRing
cring_Z $-> R
Proof.
R: CRing
cring_Z $-> R
  snrapply Build_RingHomomorphism.
R: CRing
cring_Z -> R
R: CRing
abstract_algebra.IsSemiRingPreserving ?rng_homo_map
  1: exact (cring_catamorphism_fun R).
R: CRing
abstract_algebra.IsSemiRingPreserving
  (cring_catamorphism_fun R)
  repeat split; exact _.
Defined.

(** The integers are the initial commutative ring *)
Global Instance isinitial_cring_Z : IsInitial cring_Z.
IsInitial cring_Z
Proof.
IsInitial cring_Z
  unfold IsInitial.
forall y : CRing,
{f : cring_Z $-> y &
forall g : cring_Z $-> y, f $== g}
  intro R.
R: CRing
{f : cring_Z $-> R &
forall g : cring_Z $-> R, f $== g}
  exists (rng_homo_int R).
R: CRing
forall g : cring_Z $-> R, rng_homo_int R $== g
  intros g x.
R: CRing
g: cring_Z $-> R
x: cring_Z
rng_homo_int R x = g x
  destruct x as [n| |p].
R: CRing
g: cring_Z $-> R
n: Pos
rng_homo_int R (neg n) = g (neg n)
R: CRing
g: cring_Z $-> R
rng_homo_int R 0%int = g 0%int
R: CRing
g: cring_Z $-> R
p: Pos
rng_homo_int R (pos p) = g (pos p)
  +
R: CRing
g: cring_Z $-> R
n: Pos
rng_homo_int R (neg n) = g (neg n) induction n using pos_peano_ind.
R: CRing
g: cring_Z $-> R
rng_homo_int R (-1)%int = g (-1)%int
R: CRing
g: cring_Z $-> R
n: Pos
IHn: rng_homo_int R (neg n) = g (neg n)
rng_homo_int R (neg (pos_succ n)) =
g (neg (pos_succ n))
    {
R: CRing
g: cring_Z $-> R
rng_homo_int R (-1)%int = g (-1)%int cbn.
R: CRing
g: cring_Z $-> R
-1 = g (-1)%int symmetry; rapply (rng_homo_minus_one (B:=R)). }
R: CRing
g: cring_Z $-> R
n: Pos
IHn: rng_homo_int R (neg n) = g (neg n)
rng_homo_int R (neg (pos_succ n)) =
g (neg (pos_succ n))
    simpl.
R: CRing
g: cring_Z $-> R
n: Pos
IHn: rng_homo_int R (neg n) = g (neg n)
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) (pos_succ n) =
g (neg (pos_succ n))
    rewrite pos_peano_rec_beta_pos_succ.
R: CRing
g: cring_Z $-> R
n: Pos
IHn: rng_homo_int R (neg n) = g (neg n)
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) n =
g (neg (pos_succ n))
    rewrite int_neg_pos_succ.
R: CRing
g: cring_Z $-> R
n: Pos
IHn: rng_homo_int R (neg n) = g (neg n)
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) n =
g (int_pred (neg n))
    unfold int_pred.
R: CRing
g: cring_Z $-> R
n: Pos
IHn: rng_homo_int R (neg n) = g (neg n)
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) n =
g (neg n + -1)%int
    rewrite int_add_comm.
R: CRing
g: cring_Z $-> R
n: Pos
IHn: rng_homo_int R (neg n) = g (neg n)
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) n =
g (-1 + neg n)%int
    rewrite rng_homo_plus.
R: CRing
g: cring_Z $-> R
n: Pos
IHn: rng_homo_int R (neg n) = g (neg n)
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) n =
g (-1)%int + g (neg n)
    rewrite rng_homo_minus_one.
R: CRing
g: cring_Z $-> R
n: Pos
IHn: rng_homo_int R (neg n) = g (neg n)
-1 +
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) n =
-1 + g (neg n)
    apply ap.
R: CRing
g: cring_Z $-> R
n: Pos
IHn: rng_homo_int R (neg n) = g (neg n)
pos_peano_rec R (-1)
  (fun (_ : Pos) (nr : R) => -1 + nr) n = g (neg n)
    exact IHn.
  +
R: CRing
g: cring_Z $-> R
rng_homo_int R 0%int = g 0%int by rewrite 2 rng_homo_zero.
  +
R: CRing
g: cring_Z $-> R
p: Pos
rng_homo_int R (pos p) = g (pos p) induction p using pos_peano_ind.
R: CRing
g: cring_Z $-> R
rng_homo_int R 1%int = g 1%int
R: CRing
g: cring_Z $-> R
p: Pos
IHp: rng_homo_int R (pos p) = g (pos p)
rng_homo_int R (pos (pos_succ p)) =
g (pos (pos_succ p))
    {
R: CRing
g: cring_Z $-> R
rng_homo_int R 1%int = g 1%int cbn.
R: CRing
g: cring_Z $-> R
1 = g 1%int symmetry; rapply (rng_homo_one g). }
R: CRing
g: cring_Z $-> R
p: Pos
IHp: rng_homo_int R (pos p) = g (pos p)
rng_homo_int R (pos (pos_succ p)) =
g (pos (pos_succ p))
    simpl.
R: CRing
g: cring_Z $-> R
p: Pos
IHp: rng_homo_int R (pos p) = g (pos p)
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr)
  (pos_succ p) = g (pos (pos_succ p))
    rewrite pos_peano_rec_beta_pos_succ.
R: CRing
g: cring_Z $-> R
p: Pos
IHp: rng_homo_int R (pos p) = g (pos p)
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) p =
g (pos (pos_succ p))
    rewrite int_pos_pos_succ.
R: CRing
g: cring_Z $-> R
p: Pos
IHp: rng_homo_int R (pos p) = g (pos p)
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) p =
g (int_succ (pos p))
    unfold int_succ.
R: CRing
g: cring_Z $-> R
p: Pos
IHp: rng_homo_int R (pos p) = g (pos p)
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) p =
g (pos p + 1)%int
    rewrite int_add_comm.
R: CRing
g: cring_Z $-> R
p: Pos
IHp: rng_homo_int R (pos p) = g (pos p)
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) p =
g (1 + pos p)%int
    rewrite rng_homo_plus.
R: CRing
g: cring_Z $-> R
p: Pos
IHp: rng_homo_int R (pos p) = g (pos p)
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) p =
g 1%int + g (pos p)
    rewrite rng_homo_one.
R: CRing
g: cring_Z $-> R
p: Pos
IHp: rng_homo_int R (pos p) = g (pos p)
1 +
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) p =
1 + g (pos p)
    apply ap.
R: CRing
g: cring_Z $-> R
p: Pos
IHp: rng_homo_int R (pos p) = g (pos p)
pos_peano_rec R 1 (fun (_ : Pos) (nr : R) => 1 + nr) p =
g (pos p)
    exact IHp.
Defined.