Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe.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.

Unset Elimination Schemes.
Set Universe Minimization ToSet.

Declare Scope int_scope.
Delimit Scope int_scope with int.
Local Open Scope int_scope.

(** * The Integers *)

(** ** Definition *)

(** We define the integers as two copies of [nat] stuck together around a [zero]. *)
Inductive Int : Type0 :=
| negS : nat -> Int
| zero : Int
| posS : nat -> Int.

(** We can convert a [nat] to an [Int] by mapping [0] to [zero] and [S n] to [posS n]. Various operations on [nat] are preserved by this function. See the section on conversion functions starting with [int_nat_succ]. *)
Definition int_of_nat (n : nat) :=
  match n with
  | O => zero
  | S n => posS n
  end.

(** We declare this conversion as a coercion so we can freely use [nat]s in statements about integers. *)
Coercion int_of_nat : nat >-> Int.

(** ** Number Notations *)

(** Here we define some printing and parsing functions that convert the integers between numeral representations so that we can use notations such as [123] for [posS 122] and [-123] for [negS 122]. *)

(** Printing *)
Definition int_to_number_int (n : Int) : Numeral.int :=
  match n with
  | posS n => Numeral.IntDec (Decimal.Pos (Nat.to_uint (S n)))
  | zero => Numeral.IntDec (Decimal.Pos (Nat.to_uint 0))
  | negS n => Numeral.IntDec (Decimal.Neg (Nat.to_uint (S n)))
  end.

(** Parsing *)
Definition int_of_number_int (d : Numeral.int) :=
  match d with
  | Numeral.IntDec (Decimal.Pos d) => int_of_nat (Nat.of_uint d)
  | Numeral.IntDec (Decimal.Neg d) => negS (nat_pred (Nat.of_uint d))
  | Numeral.IntHex (Hexadecimal.Pos u) => int_of_nat (Nat.of_hex_uint u)
  | Numeral.IntHex (Hexadecimal.Neg u) => negS (nat_pred (Nat.of_hex_uint u))
  end.

Number Notation Int int_of_number_int int_to_number_int : int_scope.

(** ** Successor, Predecessor and Negation *)

(** These operations will be used in the induction principle we derive for [Int] so we need to define them early on. *)

(** *** Successor and Predecessor *)

Definition int_succ (n : Int) : Int :=
  match n with
  | posS n => posS (S n)
  | 0 => 1
  | -1 => 0
  | negS (S n) => negS n
  end.

Notation "n .+1" := (int_succ n) : int_scope.

Definition int_pred (n : Int) : Int :=
  match n with
  | posS (S n) => posS n
  | 1 => 0 
  | 0 => -1
  | negS n => negS (S n)
  end.

Notation "n .-1" := (int_pred n) : int_scope.

(** *** Negation *)

Definition int_neg@{} (x : Int) : Int :=
  match x with
  | posS x => negS x
  | zero => zero
  | negS x => posS x
  end.

Notation "- x" := (int_neg x) : int_scope.

(** ** Basic Properties *)

(** *** Integer induction *)

(** The induction principle for integers is similar to the induction principle for natural numbers. However we have two induction hypotheses going in either direction starting from 0. *)
Definition Int_ind@{i} (P : Int -> Type@{i})
  (H0 : P 0)
  (HP : forall n : nat, P n -> P (int_succ n))
  (HN : forall n : nat, P (- n) -> P (int_pred (-n)))
  : forall x, P x.
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
forall x : Int, P x
Proof.
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
forall x : Int, P x
  intros[x | | x].
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
x: nat
P (negS x)
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
P 0
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
x: nat
P (posS x)
  -
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
x: nat
P (negS x) induction x as [|x IHx].
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
P (-1)
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
x: nat
IHx: P (negS x)
P (negS x.+1)
    +
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
P (-1) apply (HN 0%nat), H0.
    +
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
x: nat
IHx: P (negS x)
P (negS x.+1) apply (HN x.+1%nat), IHx.
  -
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
P 0 exact H0.
  -
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
x: nat
P (posS x) induction x as [|x IHx].
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
P 1
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
x: nat
IHx: P (posS x)
P (posS x.+1)
    *
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
P 1 apply (HP 0%nat), H0.
    *
P: Int -> Type
H0: P 0
HP: forall n : nat, P n -> P n.+1
HN: forall n : nat, P (- n) -> P (- n).-1
x: nat
IHx: P (posS x)
P (posS x.+1) apply (HP x.+1%nat), IHx.
Defined.

(** We record these so that they can be used with the [induction] tactic. *)
Definition Int_rect := Int_ind.
Definition Int_rec := Int_ind.

(** *** Decidable Equality *)

(** The integers have decidable equality. *)
Instance decidable_paths_int@{} : DecidablePaths Int.
DecidablePaths Int
Proof.
DecidablePaths Int
  intros x y.
x, y: Int
Decidable (x = y)
  destruct x as [x | | x], y as [y |  | y].
x, y: nat
Decidable (negS x = negS y)
x: nat
Decidable (negS x = 0)
x, y: nat
Decidable (negS x = posS y)
y: nat
Decidable (0 = negS y)
Decidable (0 = 0)
y: nat
Decidable (0 = posS y)
x, y: nat
Decidable (posS x = negS y)
x: nat
Decidable (posS x = 0)
x, y: nat
Decidable (posS x = posS y)
  2-4,6-8: right; intros; discriminate.
x, y: nat
Decidable (negS x = negS y)
Decidable (0 = 0)
x, y: nat
Decidable (posS x = posS y)
  2: by left.
x, y: nat
Decidable (negS x = negS y)
x, y: nat
Decidable (posS x = posS y)
  1,2: napply decidable_iff.
x, y: nat
Iff.iff ?Goal (negS x = negS y)
x, y: nat
Decidable ?Goal
x, y: nat
Iff.iff ?Goal2 (posS x = posS y)
x, y: nat
Decidable ?Goal2
  1,3: split.
x, y: nat
?Goal -> negS x = negS y
x, y: nat
negS x = negS y -> ?Goal
x, y: nat
?Goal1 -> posS x = posS y
x, y: nat
posS x = posS y -> ?Goal1
x, y: nat
Decidable ?Goal
x, y: nat
Decidable ?Goal1
  1,3: napply ap.
x, y: nat
negS x = negS y -> x = y
x, y: nat
posS x = posS y -> x = y
x, y: nat
Decidable (x = y)
x, y: nat
Decidable (x = y)
  1,2: intros H; by injection H.
x, y: nat
Decidable (x = y)
x, y: nat
Decidable (x = y)
  1,2: exact _.
Defined.

(** By Hedberg's theorem, we have that the integers are a set. *)
Instance ishset_int@{} : IsHSet Int := _.

(** *** Pointedness *)

(** We sometimes want to treat the integers as a pointed type with basepoint given by 0. *)
Instance ispointed_int : IsPointed Int := 0.

(** ** Operations *)

(** *** Addition *)

(** Addition for integers is defined by integer induction on the first argument. *)
Definition int_add@{} (x y : Int) : Int.
x, y: Int
Int
Proof.
x, y: Int
Int
  induction x as [|x IHx|x IHx] in y |- *.
y: Int
Int
x: nat
y: Int
IHx: Int -> Int
Int
x: nat
y: Int
IHx: Int -> Int
Int
  (** [0 + y = y] *)
  -
y: Int
Int exact y.
  (** [x.+1 + y = (x + y).+1] *)
  -
x: nat
y: Int
IHx: Int -> Int
Int exact (int_succ (IHx y)).
  (** [x.-1 + y = (x + y).-1] *)
  -
x: nat
y: Int
IHx: Int -> Int
Int exact (int_pred (IHx y)).
Defined.

Infix "+" := int_add : int_scope.
Infix "-" := (fun x y => x + -y) : int_scope.

(** *** Multiplication *)

(** Multiplication for integers is defined by integer induction on the first argument. *)
Definition int_mul@{} (x y : Int) : Int.
x, y: Int
Int
Proof.
x, y: Int
Int
  induction x as [|x IHx|x IHx] in y |- *.
y: Int
Int
x: nat
y: Int
IHx: Int -> Int
Int
x: nat
y: Int
IHx: Int -> Int
Int
  (** [0 * y = 0] *)
  -
y: Int
Int exact 0.
  (** [x.+1 * y = y + x * y] *)
  -
x: nat
y: Int
IHx: Int -> Int
Int exact (y + IHx y).
  (** [x.-1 * y = -y + x * y] *)
  -
x: nat
y: Int
IHx: Int -> Int
Int exact (-y + IHx y).
Defined.

Infix "*" := int_mul : int_scope.

(** ** Properties of Operations *)

(** *** Negation *)

(** Negation is involutive. *)
Definition int_neg_neg@{} (x : Int) : - - x = x.
x: Int
- - x = x  
Proof.
x: Int
- - x = x
  by destruct x.
Defined.

(** Negation is an equivalence. *)
Instance isequiv_int_neg@{} : IsEquiv int_neg.
IsEquiv int_neg
Proof.
IsEquiv int_neg
  snapply (isequiv_adjointify int_neg int_neg).
int_neg o int_neg == idmap
int_neg o int_neg == idmap
  1,2: exact int_neg_neg.
Defined.

(** Negation is injective. *)
Definition isinj_int_neg@{} (x y : Int) : - x = - y -> x = y
  := equiv_inj int_neg.

(** The negation of a successor is the predecessor of the negation. *)
Definition int_neg_succ (x : Int) : - x.+1 = (- x).-1.
x: Int
- x.+1 = (- x).-1
Proof.
x: Int
- x.+1 = (- x).-1
  by destruct x as [[] | | ].
Defined.

(** The negation of a predecessor is the successor of the negation. *)
Definition int_neg_pred (x : Int) : - x.-1 = (- x).+1.
x: Int
- x.-1 = (- x).+1
Proof.
x: Int
- x.-1 = (- x).+1
  by destruct x as [ | | []].
Defined.

(** The successor of a predecessor is the identity. *)
Definition int_pred_succ@{} (x : Int) : x.-1.+1 = x.
x: Int
x.-1.+1 = x
Proof.
x: Int
x.-1.+1 = x
  by destruct x as [ | | []].
Defined. 

(** The predecessor of a successor is the identity. *)
Definition int_succ_pred@{} (x : Int) : x.+1.-1 = x.
x: Int
x.+1.-1 = x
Proof.
x: Int
x.+1.-1 = x
  by destruct x as [[] | | ].
Defined.

(** The successor is an equivalence on [Int] *)
Instance isequiv_int_succ@{} : IsEquiv int_succ
  := isequiv_adjointify int_succ int_pred int_pred_succ int_succ_pred.

(** The predecessor is an equivalence on [Int] *)
Instance isequiv_int_pred@{} : IsEquiv int_pred
  := isequiv_inverse int_succ.

(** *** Addition *)

(** Integer addition with zero on the left is the identity by definition. *)
Definition int_add_0_l@{} (x : Int) : 0 + x = x := 1.

(** Integer addition with zero on the right is the identity. *)
Definition int_add_0_r@{} (x : Int) : x + 0 = x.
x: Int
x + 0 = x
Proof.
x: Int
x + 0 = x
  induction x as [|[|x] IHx|[|x] IHx].
0 + 0 = 0
IHx: 0%nat + 0 = 0%nat
0%nat.+1 + 0 = 0%nat.+1
x: nat
IHx: x.+1%nat + 0 = x.+1%nat
x.+1%nat.+1 + 0 = x.+1%nat.+1
IHx: - 0%nat + 0 = - 0%nat
(- 0%nat).-1 + 0 = (- 0%nat).-1
x: nat
IHx: - x.+1%nat + 0 = - x.+1%nat
(- x.+1%nat).-1 + 0 = (- x.+1%nat).-1
  -
0 + 0 = 0 reflexivity.
  -
IHx: 0%nat + 0 = 0%nat
0%nat.+1 + 0 = 0%nat.+1 reflexivity.
  -
x: nat
IHx: x.+1%nat + 0 = x.+1%nat
x.+1%nat.+1 + 0 = x.+1%nat.+1 change (?z.+1 + 0) with (z + 0).+1.
x: nat
IHx: x.+1%nat + 0 = x.+1%nat
(x.+1%nat + 0).+1 = x.+1%nat.+1
    exact (ap _ IHx).
  -
IHx: - 0%nat + 0 = - 0%nat
(- 0%nat).-1 + 0 = (- 0%nat).-1 reflexivity.
  -
x: nat
IHx: - x.+1%nat + 0 = - x.+1%nat
(- x.+1%nat).-1 + 0 = (- x.+1%nat).-1 change (?z.-1 + 0) with (z + 0).-1.
x: nat
IHx: - x.+1%nat + 0 = - x.+1%nat
(- x.+1%nat + 0).-1 = (- x.+1%nat).-1
    exact (ap _ IHx).
Defined. 

(** Adding a successor on the left is the successor of the sum. *)
Definition int_add_succ_l@{} (x y : Int) : x.+1 + y = (x + y).+1.
x, y: Int
x.+1 + y = (x + y).+1
Proof.
x, y: Int
x.+1 + y = (x + y).+1
  induction x as [|[|x] IHx|[|x] IHx] in y |- *.
y: Int
0.+1 + y = (0 + y).+1
y: Int
IHx: forall y0 : Int, 0%nat.+1 + y0 = (0%nat + y0).+1
0%nat.+1.+1 + y = (0%nat.+1 + y).+1
x: nat
y: Int
IHx: forall y0 : Int, x.+1%nat.+1 + y0 = (x.+1%nat + y0).+1
x.+1%nat.+1.+1 + y = (x.+1%nat.+1 + y).+1
y: Int
IHx: forall y0 : Int, (- 0%nat).+1 + y0 = (- 0%nat + y0).+1
(- 0%nat).-1.+1 + y = ((- 0%nat).-1 + y).+1
x: nat
y: Int
IHx: forall y0 : Int, (- x.+1%nat).+1 + y0 = (- x.+1%nat + y0).+1
(- x.+1%nat).-1.+1 + y = ((- x.+1%nat).-1 + y).+1
  1-3: reflexivity.
y: Int
IHx: forall y0 : Int, (- 0%nat).+1 + y0 = (- 0%nat + y0).+1
(- 0%nat).-1.+1 + y = ((- 0%nat).-1 + y).+1
x: nat
y: Int
IHx: forall y0 : Int, (- x.+1%nat).+1 + y0 = (- x.+1%nat + y0).+1
(- x.+1%nat).-1.+1 + y = ((- x.+1%nat).-1 + y).+1
  all: symmetry; apply int_pred_succ.
Defined.

(** Adding a predecessor on the left is the predecessor of the sum. *)
Definition int_add_pred_l@{} (x y : Int) : x.-1 + y = (x + y).-1.
x, y: Int
x.-1 + y = (x + y).-1
Proof.
x, y: Int
x.-1 + y = (x + y).-1
  induction x as [|[|x] IHx|[|x] IHx] in y |- *.
y: Int
0.-1 + y = (0 + y).-1
y: Int
IHx: forall y0 : Int, 0%nat.-1 + y0 = (0%nat + y0).-1
0%nat.+1.-1 + y = (0%nat.+1 + y).-1
x: nat
y: Int
IHx: forall y0 : Int, x.+1%nat.-1 + y0 = (x.+1%nat + y0).-1
x.+1%nat.+1.-1 + y = (x.+1%nat.+1 + y).-1
y: Int
IHx: forall y0 : Int, (- 0%nat).-1 + y0 = (- 0%nat + y0).-1
(- 0%nat).-1.-1 + y = ((- 0%nat).-1 + y).-1
x: nat
y: Int
IHx: forall y0 : Int, (- x.+1%nat).-1 + y0 = (- x.+1%nat + y0).-1
(- x.+1%nat).-1.-1 + y = ((- x.+1%nat).-1 + y).-1
  1,4,5: reflexivity.
y: Int
IHx: forall y0 : Int, 0%nat.-1 + y0 = (0%nat + y0).-1
0%nat.+1.-1 + y = (0%nat.+1 + y).-1
x: nat
y: Int
IHx: forall y0 : Int, x.+1%nat.-1 + y0 = (x.+1%nat + y0).-1
x.+1%nat.+1.-1 + y = (x.+1%nat.+1 + y).-1
  all: symmetry; apply int_succ_pred.
Defined.

(** Adding a successor on the right is the successor of the sum. *)
Definition int_add_succ_r@{} (x y : Int) : x + y.+1 = (x + y).+1.
x, y: Int
x + y.+1 = (x + y).+1
Proof.
x, y: Int
x + y.+1 = (x + y).+1
  induction x as [|x IHx|[] IHx] in y |- *.
y: Int
0 + y.+1 = (0 + y).+1
x: nat
y: Int
IHx: forall y0 : Int, x + y0.+1 = (x + y0).+1
x.+1 + y.+1 = (x.+1 + y).+1
y: Int
IHx: forall y0 : Int, - 0%nat + y0.+1 = (- 0%nat + y0).+1
(- 0%nat).-1 + y.+1 = ((- 0%nat).-1 + y).+1
n: nat
y: Int
IHx: forall y0 : Int, - n.+1%nat + y0.+1 = (- n.+1%nat + y0).+1
(- n.+1%nat).-1 + y.+1 = ((- n.+1%nat).-1 + y).+1
  -
y: Int
0 + y.+1 = (0 + y).+1 reflexivity.
  -
x: nat
y: Int
IHx: forall y0 : Int, x + y0.+1 = (x + y0).+1
x.+1 + y.+1 = (x.+1 + y).+1 by rewrite 2 int_add_succ_l, IHx.
  -
y: Int
IHx: forall y0 : Int, - 0%nat + y0.+1 = (- 0%nat + y0).+1
(- 0%nat).-1 + y.+1 = ((- 0%nat).-1 + y).+1 cbn; by rewrite int_succ_pred, int_pred_succ.
  -
n: nat
y: Int
IHx: forall y0 : Int, - n.+1%nat + y0.+1 = (- n.+1%nat + y0).+1
(- n.+1%nat).-1 + y.+1 = ((- n.+1%nat).-1 + y).+1 change ((- (n.+1%nat)).-1 + y.+1 = ((- (n.+1%nat)).-1 + y).+1).
n: nat
y: Int
IHx: forall y0 : Int, - n.+1%nat + y0.+1 = (- n.+1%nat + y0).+1
(- n.+1%nat).-1 + y.+1 = ((- n.+1%nat).-1 + y).+1
    rewrite int_add_pred_l.
n: nat
y: Int
IHx: forall y0 : Int, - n.+1%nat + y0.+1 = (- n.+1%nat + y0).+1
(- n.+1%nat + y.+1).-1 = ((- n.+1%nat).-1 + y).+1
    rewrite IHx.
n: nat
y: Int
IHx: forall y0 : Int, - n.+1%nat + y0.+1 = (- n.+1%nat + y0).+1
(- n.+1%nat + y).+1.-1 = ((- n.+1%nat).-1 + y).+1
    rewrite <- 2 int_add_succ_l.
n: nat
y: Int
IHx: forall y0 : Int, - n.+1%nat + y0.+1 = (- n.+1%nat + y0).+1
((- n.+1%nat).+1 + y).-1 = (- n.+1%nat).-1.+1 + y
    rewrite <- int_add_pred_l.
n: nat
y: Int
IHx: forall y0 : Int, - n.+1%nat + y0.+1 = (- n.+1%nat + y0).+1
(- n.+1%nat).+1.-1 + y = (- n.+1%nat).-1.+1 + y
    by rewrite int_pred_succ, int_succ_pred.
Defined.

(** Adding a predecessor on the right is the predecessor of the sum. *)
Definition int_add_pred_r (x y : Int) : x + y.-1 = (x + y).-1.
x, y: Int
x + y.-1 = (x + y).-1
Proof.
x, y: Int
x + y.-1 = (x + y).-1
  induction x as [|x IHx|[] IHx] in y |- *.
y: Int
0 + y.-1 = (0 + y).-1
x: nat
y: Int
IHx: forall y0 : Int, x + y0.-1 = (x + y0).-1
x.+1 + y.-1 = (x.+1 + y).-1
y: Int
IHx: forall y0 : Int, - 0%nat + y0.-1 = (- 0%nat + y0).-1
(- 0%nat).-1 + y.-1 = ((- 0%nat).-1 + y).-1
n: nat
y: Int
IHx: forall y0 : Int, - n.+1%nat + y0.-1 = (- n.+1%nat + y0).-1
(- n.+1%nat).-1 + y.-1 = ((- n.+1%nat).-1 + y).-1
  -
y: Int
0 + y.-1 = (0 + y).-1 reflexivity.
  -
x: nat
y: Int
IHx: forall y0 : Int, x + y0.-1 = (x + y0).-1
x.+1 + y.-1 = (x.+1 + y).-1 rewrite 2 int_add_succ_l.
x: nat
y: Int
IHx: forall y0 : Int, x + y0.-1 = (x + y0).-1
(x + y.-1).+1 = (x + y).+1.-1
    rewrite IHx.
x: nat
y: Int
IHx: forall y0 : Int, x + y0.-1 = (x + y0).-1
(x + y).-1.+1 = (x + y).+1.-1
    by rewrite int_pred_succ, int_succ_pred.
  -
y: Int
IHx: forall y0 : Int, - 0%nat + y0.-1 = (- 0%nat + y0).-1
(- 0%nat).-1 + y.-1 = ((- 0%nat).-1 + y).-1 reflexivity.
  -
n: nat
y: Int
IHx: forall y0 : Int, - n.+1%nat + y0.-1 = (- n.+1%nat + y0).-1
(- n.+1%nat).-1 + y.-1 = ((- n.+1%nat).-1 + y).-1 rewrite 2 int_add_pred_l.
n: nat
y: Int
IHx: forall y0 : Int, - n.+1%nat + y0.-1 = (- n.+1%nat + y0).-1
(- n.+1%nat + y.-1).-1 = (- n.+1%nat + y).-1.-1
    by rewrite IHx.
Defined.

(** Integer addition is commutative. *)
Definition int_add_comm@{} (x y : Int) : x + y = y + x.
x, y: Int
x + y = y + x
Proof.
x, y: Int
x + y = y + x
  induction y as [|y IHy|y IHy] in x |- *.
x: Int
x + 0 = 0 + x
x: Int
y: nat
IHy: forall x0 : Int, x0 + y = y + x0
x + y.+1 = y.+1 + x
x: Int
y: nat
IHy: forall x0 : Int, x0 + - y = - y + x0
x + (- y).-1 = (- y).-1 + x
  -
x: Int
x + 0 = 0 + x apply int_add_0_r.
  -
x: Int
y: nat
IHy: forall x0 : Int, x0 + y = y + x0
x + y.+1 = y.+1 + x rewrite int_add_succ_l.
x: Int
y: nat
IHy: forall x0 : Int, x0 + y = y + x0
x + y.+1 = (y + x).+1
    rewrite <- IHy.
x: Int
y: nat
IHy: forall x0 : Int, x0 + y = y + x0
x + y.+1 = (x + y).+1
    by rewrite int_add_succ_r.
  -
x: Int
y: nat
IHy: forall x0 : Int, x0 + - y = - y + x0
x + (- y).-1 = (- y).-1 + x rewrite int_add_pred_r.
x: Int
y: nat
IHy: forall x0 : Int, x0 + - y = - y + x0
(x + - y).-1 = (- y).-1 + x
    rewrite int_add_pred_l.
x: Int
y: nat
IHy: forall x0 : Int, x0 + - y = - y + x0
(x + - y).-1 = (- y + x).-1
    f_ap.
Defined.

(** Integer addition is associative. *)
Definition int_add_assoc@{} (x y z : Int) : x + (y + z) = x + y + z.
x, y, z: Int
x + (y + z) = x + y + z
Proof.
x, y, z: Int
x + (y + z) = x + y + z
  induction x as [|x IHx|x IHx] in y, z |- *.
y, z: Int
0 + (y + z) = 0 + y + z
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x + (y0 + z0) = x + y0 + z0
x.+1 + (y + z) = x.+1 + y + z
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x + (y0 + z0) = - x + y0 + z0
(- x).-1 + (y + z) = (- x).-1 + y + z
  -
y, z: Int
0 + (y + z) = 0 + y + z reflexivity.
  -
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x + (y0 + z0) = x + y0 + z0
x.+1 + (y + z) = x.+1 + y + z by rewrite !int_add_succ_l, IHx.
  -
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x + (y0 + z0) = - x + y0 + z0
(- x).-1 + (y + z) = (- x).-1 + y + z by rewrite !int_add_pred_l, IHx.
Defined.

(** Negation is a left inverse with respect to integer addition. *)
Definition int_add_neg_l@{} (x : Int) : - x + x = 0.
x: Int
- x + x = 0
Proof.
x: Int
- x + x = 0
  induction x as [|x IHx|x IHx].
- 0 + 0 = 0
x: nat
IHx: - x + x = 0
- x.+1 + x.+1 = 0
x: nat
IHx: - - x + - x = 0
- (- x).-1 + (- x).-1 = 0
  -
- 0 + 0 = 0 reflexivity.
  -
x: nat
IHx: - x + x = 0
- x.+1 + x.+1 = 0 by rewrite int_neg_succ, int_add_pred_l, int_add_succ_r, IHx.
  -
x: nat
IHx: - - x + - x = 0
- (- x).-1 + (- x).-1 = 0 by rewrite int_neg_pred, int_add_succ_l, int_add_pred_r, IHx.
Defined.

(** Negation is a right inverse with respect to integer addition. *)
Definition int_add_neg_r@{} (x : Int) : x - x = 0.
x: Int
x - x = 0
Proof.
x: Int
x - x = 0
  unfold "-"; by rewrite int_add_comm, int_add_neg_l.
Defined.

(** Negation distributes over addition. *)
Definition int_neg_add@{} (x y : Int) : - (x + y) = - x - y.
x, y: Int
- (x + y) = - x - y
Proof.
x, y: Int
- (x + y) = - x - y
  induction x as [|x IHx|x IHx] in y |- *.
y: Int
- (0 + y) = - 0 + - y
x: nat
y: Int
IHx: forall y0 : Int, - (x + y0) = - x + - y0
- (x.+1 + y) = - x.+1 + - y
x: nat
y: Int
IHx: forall y0 : Int, - (- x + y0) = - - x + - y0
- ((- x).-1 + y) = - (- x).-1 + - y
  -
y: Int
- (0 + y) = - 0 + - y reflexivity.
  -
x: nat
y: Int
IHx: forall y0 : Int, - (x + y0) = - x + - y0
- (x.+1 + y) = - x.+1 + - y rewrite int_add_succ_l.
x: nat
y: Int
IHx: forall y0 : Int, - (x + y0) = - x + - y0
- (x + y).+1 = - x.+1 + - y
    rewrite 2 int_neg_succ.
x: nat
y: Int
IHx: forall y0 : Int, - (x + y0) = - x + - y0
(- (x + y)).-1 = (- x).-1 + - y
    rewrite int_add_pred_l.
x: nat
y: Int
IHx: forall y0 : Int, - (x + y0) = - x + - y0
(- (x + y)).-1 = (- x + - y).-1
    f_ap.
  -
x: nat
y: Int
IHx: forall y0 : Int, - (- x + y0) = - - x + - y0
- ((- x).-1 + y) = - (- x).-1 + - y rewrite int_neg_pred.
x: nat
y: Int
IHx: forall y0 : Int, - (- x + y0) = - - x + - y0
- ((- x).-1 + y) = (- - x).+1 + - y
    rewrite int_add_succ_l.
x: nat
y: Int
IHx: forall y0 : Int, - (- x + y0) = - - x + - y0
- ((- x).-1 + y) = (- - x + - y).+1
    rewrite int_add_pred_l.
x: nat
y: Int
IHx: forall y0 : Int, - (- x + y0) = - - x + - y0
- (- x + y).-1 = (- - x + - y).+1
    rewrite int_neg_pred.
x: nat
y: Int
IHx: forall y0 : Int, - (- x + y0) = - - x + - y0
(- (- x + y)).+1 = (- - x + - y).+1
    f_ap.
Defined.
      
(** *** Multiplication *)

(** Multiplication with a successor on the left is the sum of the multiplication without the successor and the multiplicand which was not a successor. *)
Definition int_mul_succ_l@{} (x y : Int) : x.+1 * y = y + x * y.
x, y: Int
x.+1 * y = y + x * y
Proof.
x, y: Int
x.+1 * y = y + x * y
  induction x as [|[|x] IHx|[] IHx] in y |- *.
y: Int
0.+1 * y = y + 0 * y
y: Int
IHx: forall y0 : Int, 0%nat.+1 * y0 = y0 + 0%nat * y0
0%nat.+1.+1 * y = y + 0%nat.+1 * y
x: nat
y: Int
IHx: forall y0 : Int, x.+1%nat.+1 * y0 = y0 + x.+1%nat * y0
x.+1%nat.+1.+1 * y = y + x.+1%nat.+1 * y
y: Int
IHx: forall y0 : Int, (- 0%nat).+1 * y0 = y0 + - 0%nat * y0
(- 0%nat).-1.+1 * y = y + (- 0%nat).-1 * y
n: nat
y: Int
IHx: forall y0 : Int, (- n.+1%nat).+1 * y0 = y0 + - n.+1%nat * y0
(- n.+1%nat).-1.+1 * y = y + (- n.+1%nat).-1 * y
  -
y: Int
0.+1 * y = y + 0 * y reflexivity.
  -
y: Int
IHx: forall y0 : Int, 0%nat.+1 * y0 = y0 + 0%nat * y0
0%nat.+1.+1 * y = y + 0%nat.+1 * y reflexivity.
  -
x: nat
y: Int
IHx: forall y0 : Int, x.+1%nat.+1 * y0 = y0 + x.+1%nat * y0
x.+1%nat.+1.+1 * y = y + x.+1%nat.+1 * y reflexivity.
  -
y: Int
IHx: forall y0 : Int, (- 0%nat).+1 * y0 = y0 + - 0%nat * y0
(- 0%nat).-1.+1 * y = y + (- 0%nat).-1 * y cbn.
y: Int
IHx: forall y0 : Int, (- 0%nat).+1 * y0 = y0 + - 0%nat * y0
0 = y + (- y + 0)
    rewrite int_add_0_r.
y: Int
IHx: forall y0 : Int, (- 0%nat).+1 * y0 = y0 + - 0%nat * y0
0 = y + - y
    by rewrite int_add_neg_r.
  -
n: nat
y: Int
IHx: forall y0 : Int, (- n.+1%nat).+1 * y0 = y0 + - n.+1%nat * y0
(- n.+1%nat).-1.+1 * y = y + (- n.+1%nat).-1 * y rewrite int_pred_succ.
n: nat
y: Int
IHx: forall y0 : Int, (- n.+1%nat).+1 * y0 = y0 + - n.+1%nat * y0
- n.+1%nat * y = y + (- n.+1%nat).-1 * y
    cbn.
n: nat
y: Int
IHx: forall y0 : Int, (- n.+1%nat).+1 * y0 = y0 + - n.+1%nat * y0
nat_rect (fun _ : nat => Int -> Int) (fun y0 : Int => - y0 + 0)
  (fun (_ : nat) (IHx0 : Int -> Int) (y0 : Int) => - y0 + IHx0 y0) n y =
y +
(- y +
 nat_rect (fun _ : nat => Int -> Int) (fun y0 : Int => - y0 + 0)
   (fun (_ : nat) (IHx0 : Int -> Int) (y0 : Int) => - y0 + IHx0 y0) n y)
    rewrite int_add_assoc.
n: nat
y: Int
IHx: forall y0 : Int, (- n.+1%nat).+1 * y0 = y0 + - n.+1%nat * y0
nat_rect (fun _ : nat => Int -> Int) (fun y0 : Int => - y0 + 0)
  (fun (_ : nat) (IHx0 : Int -> Int) (y0 : Int) => - y0 + IHx0 y0) n y =
y + - y +
nat_rect (fun _ : nat => Int -> Int) (fun y0 : Int => - y0 + 0)
  (fun (_ : nat) (IHx0 : Int -> Int) (y0 : Int) => - y0 + IHx0 y0) n y
    rewrite int_add_neg_r.
n: nat
y: Int
IHx: forall y0 : Int, (- n.+1%nat).+1 * y0 = y0 + - n.+1%nat * y0
nat_rect (fun _ : nat => Int -> Int) (fun y0 : Int => - y0 + 0)
  (fun (_ : nat) (IHx0 : Int -> Int) (y0 : Int) => - y0 + IHx0 y0) n y =
0 +
nat_rect (fun _ : nat => Int -> Int) (fun y0 : Int => - y0 + 0)
  (fun (_ : nat) (IHx0 : Int -> Int) (y0 : Int) => - y0 + IHx0 y0) n y
    by rewrite int_add_0_l.
Defined.

(** Similarly, multiplication with a predecessor on the left is the sum of the multiplication without the predecessor and the negation of the multiplicand which was not a predecessor. *)
Definition int_mul_pred_l@{} (x y : Int) : x.-1 * y = -y + x * y.
x, y: Int
x.-1 * y = - y + x * y
Proof.
x, y: Int
x.-1 * y = - y + x * y
  induction x as [|x IHx|[] IHx] in y |- *.
y: Int
0.-1 * y = - y + 0 * y
x: nat
y: Int
IHx: forall y0 : Int, x.-1 * y0 = - y0 + x * y0
x.+1.-1 * y = - y + x.+1 * y
y: Int
IHx: forall y0 : Int, (- 0%nat).-1 * y0 = - y0 + - 0%nat * y0
(- 0%nat).-1.-1 * y = - y + (- 0%nat).-1 * y
n: nat
y: Int
IHx: forall y0 : Int, (- n.+1%nat).-1 * y0 = - y0 + - n.+1%nat * y0
(- n.+1%nat).-1.-1 * y = - y + (- n.+1%nat).-1 * y
  -
y: Int
0.-1 * y = - y + 0 * y reflexivity.
  -
x: nat
y: Int
IHx: forall y0 : Int, x.-1 * y0 = - y0 + x * y0
x.+1.-1 * y = - y + x.+1 * y rewrite int_mul_succ_l.
x: nat
y: Int
IHx: forall y0 : Int, x.-1 * y0 = - y0 + x * y0
x.+1.-1 * y = - y + (y + x * y)
    rewrite int_succ_pred.
x: nat
y: Int
IHx: forall y0 : Int, x.-1 * y0 = - y0 + x * y0
x * y = - y + (y + x * y)
    rewrite int_add_assoc.
x: nat
y: Int
IHx: forall y0 : Int, x.-1 * y0 = - y0 + x * y0
x * y = - y + y + x * y
    by rewrite int_add_neg_l.
  -
y: Int
IHx: forall y0 : Int, (- 0%nat).-1 * y0 = - y0 + - 0%nat * y0
(- 0%nat).-1.-1 * y = - y + (- 0%nat).-1 * y reflexivity.
  -
n: nat
y: Int
IHx: forall y0 : Int, (- n.+1%nat).-1 * y0 = - y0 + - n.+1%nat * y0
(- n.+1%nat).-1.-1 * y = - y + (- n.+1%nat).-1 * y reflexivity.
Defined.

(** Integer multiplication with zero on the left is zero by definition. *)
Definition int_mul_0_l@{} (x : Int) : 0 * x = 0 := 1.

(** Integer multiplication with zero on the right is zero. *)
Definition int_mul_0_r@{} (x : Int) : x * 0 = 0.
x: Int
x * 0 = 0
Proof.
x: Int
x * 0 = 0
  induction x as [|x IHx|x IHx].
0 * 0 = 0
x: nat
IHx: x * 0 = 0
x.+1 * 0 = 0
x: nat
IHx: - x * 0 = 0
(- x).-1 * 0 = 0
  -
0 * 0 = 0 reflexivity.
  -
x: nat
IHx: x * 0 = 0
x.+1 * 0 = 0 by rewrite int_mul_succ_l, int_add_0_l.
  -
x: nat
IHx: - x * 0 = 0
(- x).-1 * 0 = 0 by rewrite int_mul_pred_l, int_add_0_l.
Defined.

(** Integer multiplication with one on the left is the identity. *)
Definition int_mul_1_l@{} (x : Int) : 1 * x = x.
x: Int
1 * x = x
Proof.
x: Int
1 * x = x
  apply int_add_0_r.
Defined.

(** Integer multiplication with one on the right is the identity. *)
Definition int_mul_1_r@{} (x : Int) : x * 1 = x.
x: Int
x * 1 = x
Proof.
x: Int
x * 1 = x
  induction x as [|x IHx|x IHx].
0 * 1 = 0
x: nat
IHx: x * 1 = x
x.+1 * 1 = x.+1
x: nat
IHx: - x * 1 = - x
(- x).-1 * 1 = (- x).-1
  -
0 * 1 = 0 reflexivity.
  -
x: nat
IHx: x * 1 = x
x.+1 * 1 = x.+1 by rewrite int_mul_succ_l, IHx.
  -
x: nat
IHx: - x * 1 = - x
(- x).-1 * 1 = (- x).-1 by rewrite int_mul_pred_l, IHx.
Defined. 

(** Multiplying with a negation on the left is the same as negating the product. *)
Definition int_mul_neg_l@{} (x y : Int) : - x * y = - (x * y).
x, y: Int
- x * y = - (x * y)
Proof.
x, y: Int
- x * y = - (x * y)
  induction x as [|x IHx|x IHx] in y |- *.
y: Int
- 0 * y = - (0 * y)
x: nat
y: Int
IHx: forall y0 : Int, - x * y0 = - (x * y0)
- x.+1 * y = - (x.+1 * y)
x: nat
y: Int
IHx: forall y0 : Int, - - x * y0 = - (- x * y0)
- (- x).-1 * y = - ((- x).-1 * y)
  -
y: Int
- 0 * y = - (0 * y) reflexivity.
  -
x: nat
y: Int
IHx: forall y0 : Int, - x * y0 = - (x * y0)
- x.+1 * y = - (x.+1 * y) rewrite int_neg_succ.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0 = - (x * y0)
(- x).-1 * y = - (x.+1 * y)
    rewrite int_mul_pred_l.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0 = - (x * y0)
- y + - x * y = - (x.+1 * y)
    rewrite int_mul_succ_l.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0 = - (x * y0)
- y + - x * y = - (y + x * y)
    rewrite int_neg_add.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0 = - (x * y0)
- y + - x * y = - y + - (x * y)
    by rewrite IHx.
  -
x: nat
y: Int
IHx: forall y0 : Int, - - x * y0 = - (- x * y0)
- (- x).-1 * y = - ((- x).-1 * y) rewrite int_neg_pred.
x: nat
y: Int
IHx: forall y0 : Int, - - x * y0 = - (- x * y0)
(- - x).+1 * y = - ((- x).-1 * y)
    rewrite int_mul_succ_l.
x: nat
y: Int
IHx: forall y0 : Int, - - x * y0 = - (- x * y0)
y + - - x * y = - ((- x).-1 * y)
    rewrite int_mul_pred_l.
x: nat
y: Int
IHx: forall y0 : Int, - - x * y0 = - (- x * y0)
y + - - x * y = - (- y + - x * y)
    rewrite int_neg_add.
x: nat
y: Int
IHx: forall y0 : Int, - - x * y0 = - (- x * y0)
y + - - x * y = - - y + - (- x * y)
    rewrite IHx.
x: nat
y: Int
IHx: forall y0 : Int, - - x * y0 = - (- x * y0)
y + - (- x * y) = - - y + - (- x * y)
    by rewrite int_neg_neg.
Defined.

(** Multiplying with a successor on the right is the sum of the multiplication without the successor and the product of the multiplicand which was not a successor and the multiplicand. *)
Definition int_mul_succ_r@{} (x y : Int) : x * y.+1 = x + x * y.
x, y: Int
x * y.+1 = x + x * y
Proof.
x, y: Int
x * y.+1 = x + x * y
  induction x as [|x IHx|x IHx] in y |- *.
y: Int
0 * y.+1 = 0 + 0 * y
x: nat
y: Int
IHx: forall y0 : Int, x * y0.+1 = x + x * y0
x.+1 * y.+1 = x.+1 + x.+1 * y
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.+1 = - x + - x * y0
(- x).-1 * y.+1 = (- x).-1 + (- x).-1 * y
  -
y: Int
0 * y.+1 = 0 + 0 * y reflexivity.
  -
x: nat
y: Int
IHx: forall y0 : Int, x * y0.+1 = x + x * y0
x.+1 * y.+1 = x.+1 + x.+1 * y rewrite 2 int_mul_succ_l.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.+1 = x + x * y0
y.+1 + x * y.+1 = x.+1 + (y + x * y)
    rewrite 2 int_add_succ_l.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.+1 = x + x * y0
(y + x * y.+1).+1 = (x + (y + x * y)).+1
    f_ap.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.+1 = x + x * y0
y + x * y.+1 = x + (y + x * y)
    rewrite IHx.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.+1 = x + x * y0
y + (x + x * y) = x + (y + x * y)
    rewrite !int_add_assoc; f_ap.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.+1 = x + x * y0
y + x = x + y
    by rewrite int_add_comm.
  -
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.+1 = - x + - x * y0
(- x).-1 * y.+1 = (- x).-1 + (- x).-1 * y rewrite 2 int_mul_pred_l.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.+1 = - x + - x * y0
- y.+1 + - x * y.+1 = (- x).-1 + (- y + - x * y)
    rewrite int_neg_succ.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.+1 = - x + - x * y0
(- y).-1 + - x * y.+1 = (- x).-1 + (- y + - x * y)
    rewrite int_mul_neg_l.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.+1 = - x + - x * y0
(- y).-1 + - (x * y.+1) = (- x).-1 + (- y + - x * y)
    rewrite 2 int_add_pred_l.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.+1 = - x + - x * y0
(- y + - (x * y.+1)).-1 = (- x + (- y + - x * y)).-1
    f_ap.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.+1 = - x + - x * y0
- y + - (x * y.+1) = - x + (- y + - x * y)
    rewrite <- int_mul_neg_l.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.+1 = - x + - x * y0
- y + - x * y.+1 = - x + (- y + - x * y)
    rewrite IHx.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.+1 = - x + - x * y0
- y + (- x + - x * y) = - x + (- y + - x * y)
    rewrite !int_add_assoc; f_ap.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.+1 = - x + - x * y0
- y + - x = - x + - y
    by rewrite int_add_comm.
Defined.

(** Multiplying with a predecessor on the right is the sum of the multiplication without the predecessor and the product of the multiplicand which was not a predecessor and the negation of the multiplicand which was not a predecessor. *)
Definition int_mul_pred_r@{} (x y : Int) : x * y.-1 = -x + x * y.
x, y: Int
x * y.-1 = - x + x * y
Proof.
x, y: Int
x * y.-1 = - x + x * y
  induction x as [|x IHx|x IHx] in y |- *.
y: Int
0 * y.-1 = - 0 + 0 * y
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
x.+1 * y.-1 = - x.+1 + x.+1 * y
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.-1 = - - x + - x * y0
(- x).-1 * y.-1 = - (- x).-1 + (- x).-1 * y
  -
y: Int
0 * y.-1 = - 0 + 0 * y reflexivity.
  -
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
x.+1 * y.-1 = - x.+1 + x.+1 * y rewrite 2 int_mul_succ_l.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
y.-1 + x * y.-1 = - x.+1 + (y + x * y)
    rewrite IHx.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
y.-1 + (- x + x * y) = - x.+1 + (y + x * y)
    rewrite !int_add_assoc; f_ap.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
y.-1 + - x = - x.+1 + y
    rewrite <- (int_neg_neg y.-1).
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
- - y.-1 + - x = - x.+1 + y
    rewrite <- int_neg_add.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
- (- y.-1 + x) = - x.+1 + y
    rewrite int_neg_pred.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
- ((- y).+1 + x) = - x.+1 + y
    rewrite int_add_succ_l.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
- (- y + x).+1 = - x.+1 + y
    rewrite int_add_comm.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
- (x + - y).+1 = - x.+1 + y
    rewrite <- int_add_succ_l.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
- (x.+1 + - y) = - x.+1 + y
    rewrite int_neg_add.
x: nat
y: Int
IHx: forall y0 : Int, x * y0.-1 = - x + x * y0
- x.+1 + - - y = - x.+1 + y
    by rewrite int_neg_neg.
  -
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.-1 = - - x + - x * y0
(- x).-1 * y.-1 = - (- x).-1 + (- x).-1 * y rewrite int_neg_pred.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.-1 = - - x + - x * y0
(- x).-1 * y.-1 = (- - x).+1 + (- x).-1 * y
    rewrite int_neg_neg.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.-1 = - - x + - x * y0
(- x).-1 * y.-1 = x.+1 + (- x).-1 * y
    rewrite 2 int_mul_pred_l.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.-1 = - - x + - x * y0
- y.-1 + - x * y.-1 = x.+1 + (- y + - x * y)
    rewrite IHx.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.-1 = - - x + - x * y0
- y.-1 + (- - x + - x * y) = x.+1 + (- y + - x * y)
    rewrite !int_add_assoc; f_ap.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.-1 = - - x + - x * y0
- y.-1 + - - x = x.+1 + - y
    rewrite int_neg_pred.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.-1 = - - x + - x * y0
(- y).+1 + - - x = x.+1 + - y
    rewrite int_neg_neg.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.-1 = - - x + - x * y0
(- y).+1 + x = x.+1 + - y
    rewrite 2 int_add_succ_l; f_ap.
x: nat
y: Int
IHx: forall y0 : Int, - x * y0.-1 = - - x + - x * y0
- y + x = x + - y
    by rewrite int_add_comm.
Defined.

(** Integer multiplication is commutative. *)
Definition int_mul_comm@{} (x y : Int) : x * y = y * x.
x, y: Int
x * y = y * x
Proof.
x, y: Int
x * y = y * x
  induction y as [|y IHy|y IHy] in x |- *.
x: Int
x * 0 = 0 * x
x: Int
y: nat
IHy: forall x0 : Int, x0 * y = y * x0
x * y.+1 = y.+1 * x
x: Int
y: nat
IHy: forall x0 : Int, x0 * - y = - y * x0
x * (- y).-1 = (- y).-1 * x
  -
x: Int
x * 0 = 0 * x apply int_mul_0_r.
  -
x: Int
y: nat
IHy: forall x0 : Int, x0 * y = y * x0
x * y.+1 = y.+1 * x rewrite int_mul_succ_l.
x: Int
y: nat
IHy: forall x0 : Int, x0 * y = y * x0
x * y.+1 = x + y * x
    rewrite int_mul_succ_r.
x: Int
y: nat
IHy: forall x0 : Int, x0 * y = y * x0
x + x * y = x + y * x
    by rewrite IHy.
  -
x: Int
y: nat
IHy: forall x0 : Int, x0 * - y = - y * x0
x * (- y).-1 = (- y).-1 * x rewrite int_mul_pred_l.
x: Int
y: nat
IHy: forall x0 : Int, x0 * - y = - y * x0
x * (- y).-1 = - x + - y * x
    rewrite int_mul_pred_r.
x: Int
y: nat
IHy: forall x0 : Int, x0 * - y = - y * x0
- x + x * - y = - x + - y * x
    by rewrite IHy.
Defined.

(** Multiplying with a negation on the right is the same as negating the product. *)
Definition int_mul_neg_r@{} (x y : Int) : x * - y = - (x * y).
x, y: Int
x * - y = - (x * y)
Proof.
x, y: Int
x * - y = - (x * y)
  rewrite !(int_mul_comm x).
x, y: Int
- y * x = - (y * x)
  apply int_mul_neg_l.
Defined.

(** Multiplication distributes over addition on the left. *)
Definition int_dist_l@{} (x y z : Int) : x * (y + z) = x * y + x * z.
x, y, z: Int
x * (y + z) = x * y + x * z
Proof.
x, y, z: Int
x * (y + z) = x * y + x * z
  induction x as [|x IHx|x IHx] in y, z |- *.
y, z: Int
0 * (y + z) = 0 * y + 0 * z
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x * (y0 + z0) = x * y0 + x * z0
x.+1 * (y + z) = x.+1 * y + x.+1 * z
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 + z0) = - x * y0 + - x * z0
(- x).-1 * (y + z) = (- x).-1 * y + (- x).-1 * z
  -
y, z: Int
0 * (y + z) = 0 * y + 0 * z reflexivity.
  -
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x * (y0 + z0) = x * y0 + x * z0
x.+1 * (y + z) = x.+1 * y + x.+1 * z rewrite 3 int_mul_succ_l.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x * (y0 + z0) = x * y0 + x * z0
y + z + x * (y + z) = y + x * y + (z + x * z)
    rewrite IHx.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x * (y0 + z0) = x * y0 + x * z0
y + z + (x * y + x * z) = y + x * y + (z + x * z)
    rewrite !int_add_assoc; f_ap.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x * (y0 + z0) = x * y0 + x * z0
y + z + x * y = y + x * y + z
    rewrite <- !int_add_assoc; f_ap.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x * (y0 + z0) = x * y0 + x * z0
z + x * y = x * y + z
    by rewrite int_add_comm.
  -
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 + z0) = - x * y0 + - x * z0
(- x).-1 * (y + z) = (- x).-1 * y + (- x).-1 * z rewrite 3 int_mul_pred_l.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 + z0) = - x * y0 + - x * z0
- (y + z) + - x * (y + z) = - y + - x * y + (- z + - x * z)
    rewrite IHx.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 + z0) = - x * y0 + - x * z0
- (y + z) + (- x * y + - x * z) = - y + - x * y + (- z + - x * z)
    rewrite !int_add_assoc; f_ap.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 + z0) = - x * y0 + - x * z0
- (y + z) + - x * y = - y + - x * y + - z
    rewrite int_neg_add.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 + z0) = - x * y0 + - x * z0
- y + - z + - x * y = - y + - x * y + - z
    rewrite <- !int_add_assoc; f_ap.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 + z0) = - x * y0 + - x * z0
- z + - x * y = - x * y + - z
    by rewrite int_add_comm.
Defined.

(** Multiplication distributes over addition on the right. *)
Definition int_dist_r@{} (x y z : Int) : (x + y) * z = x * z + y * z.
x, y, z: Int
(x + y) * z = x * z + y * z
Proof.
x, y, z: Int
(x + y) * z = x * z + y * z
  by rewrite int_mul_comm, int_dist_l, !(int_mul_comm z).
Defined.

(** Multiplication is associative. *)
Definition int_mul_assoc@{} (x y z : Int) : x * (y * z) = x * y * z.
x, y, z: Int
x * (y * z) = x * y * z
Proof.
x, y, z: Int
x * (y * z) = x * y * z
  induction x as [|x IHx|x IHx] in y, z |- *.
y, z: Int
0 * (y * z) = 0 * y * z
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x * (y0 * z0) = x * y0 * z0
x.+1 * (y * z) = x.+1 * y * z
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 * z0) = - x * y0 * z0
(- x).-1 * (y * z) = (- x).-1 * y * z
  -
y, z: Int
0 * (y * z) = 0 * y * z reflexivity.
  -
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x * (y0 * z0) = x * y0 * z0
x.+1 * (y * z) = x.+1 * y * z rewrite 2 int_mul_succ_l.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x * (y0 * z0) = x * y0 * z0
y * z + x * (y * z) = (y + x * y) * z
    rewrite int_dist_r.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, x * (y0 * z0) = x * y0 * z0
y * z + x * (y * z) = y * z + x * y * z
    by rewrite IHx.
  -
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 * z0) = - x * y0 * z0
(- x).-1 * (y * z) = (- x).-1 * y * z rewrite 2 int_mul_pred_l.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 * z0) = - x * y0 * z0
- (y * z) + - x * (y * z) = (- y + - x * y) * z
    rewrite int_dist_r.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 * z0) = - x * y0 * z0
- (y * z) + - x * (y * z) = - y * z + - x * y * z
    rewrite <- int_mul_neg_l.
x: nat
y, z: Int
IHx: forall y0 z0 : Int, - x * (y0 * z0) = - x * y0 * z0
- y * z + - x * (y * z) = - y * z + - x * y * z
    by rewrite IHx.
Defined.

(** ** Iteration of equivalences *)

(** *** 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
      | zero => idmap
      | posS n => fun x => nat_iter n.+1%nat f x
     end.

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.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (- n) a = int_iter f^-1 n a
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (- n) a = int_iter f^-1 n a
  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).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f n.+1 a = f (int_iter f n a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f n.+1 a = f (int_iter f n a)
  induction n as [|n|n].
A: Type
f: A -> A
H: IsEquiv f
a: A
int_iter f 0.+1 a = f (int_iter f 0 a)
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f n.+1 a = f (int_iter f n a)
int_iter f n.+1.+1 a = f (int_iter f n.+1 a)
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f (- n).+1 a = f (int_iter f (- n) a)
int_iter f (- n).-1.+1 a = f (int_iter f (- n).-1 a)
  -
A: Type
f: A -> A
H: IsEquiv f
a: A
int_iter f 0.+1 a = f (int_iter f 0 a) reflexivity.
  -
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f n.+1 a = f (int_iter f n a)
int_iter f n.+1.+1 a = f (int_iter f n.+1 a) by destruct n.
  -
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f (- n).+1 a = f (int_iter f (- n) a)
int_iter f (- n).-1.+1 a = f (int_iter f (- n).-1 a) rewrite int_pred_succ.
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f (- n).+1 a = f (int_iter f (- n) a)
int_iter f (- n) a = f (int_iter f (- n).-1 a) 
    destruct n.
A: Type
f: A -> A
H: IsEquiv f
a: A
IHn: int_iter f (- 0%nat).+1 a = f (int_iter f (- 0%nat) a)
int_iter f (- 0%nat) a = f (int_iter f (- 0%nat).-1 a)
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f (- n.+1%nat).+1 a = f (int_iter f (- n.+1%nat) a)
int_iter f (- n.+1%nat) a = f (int_iter f (- n.+1%nat).-1 a)
    all: symmetry; apply 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).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f n.+1 a = int_iter f n (f a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f n.+1 a = int_iter f n (f a)
  induction n as [|n|n].
A: Type
f: A -> A
H: IsEquiv f
a: A
int_iter f 0.+1 a = int_iter f 0 (f a)
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f n.+1 a = int_iter f n (f a)
int_iter f n.+1.+1 a = int_iter f n.+1 (f a)
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f (- n).+1 a = int_iter f (- n) (f a)
int_iter f (- n).-1.+1 a = int_iter f (- n).-1 (f a)
  -
A: Type
f: A -> A
H: IsEquiv f
a: A
int_iter f 0.+1 a = int_iter f 0 (f a) reflexivity.
  -
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f n.+1 a = int_iter f n (f a)
int_iter f n.+1.+1 a = int_iter f n.+1 (f a) destruct n.
A: Type
f: A -> A
H: IsEquiv f
a: A
IHn: int_iter f 0%nat.+1 a = int_iter f 0%nat (f a)
int_iter f 0%nat.+1.+1 a = int_iter f 0%nat.+1 (f a)
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f n.+1%nat.+1 a = int_iter f n.+1%nat (f a)
int_iter f n.+1%nat.+1.+1 a = int_iter f n.+1%nat.+1 (f a)
    1: reflexivity.
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f n.+1%nat.+1 a = int_iter f n.+1%nat (f a)
int_iter f n.+1%nat.+1.+1 a = int_iter f n.+1%nat.+1 (f a)
    cbn; f_ap.
  -
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f (- n).+1 a = int_iter f (- n) (f a)
int_iter f (- n).-1.+1 a = int_iter f (- n).-1 (f a) destruct n.
A: Type
f: A -> A
H: IsEquiv f
a: A
IHn: int_iter f (- 0%nat).+1 a = int_iter f (- 0%nat) (f a)
int_iter f (- 0%nat).-1.+1 a = int_iter f (- 0%nat).-1 (f a)
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f (- n.+1%nat).+1 a = int_iter f (- n.+1%nat) (f a)
int_iter f (- n.+1%nat).-1.+1 a = int_iter f (- n.+1%nat).-1 (f a)
    1: symmetry; apply eissect.
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f (- n.+1%nat).+1 a = int_iter f (- n.+1%nat) (f a)
int_iter f (- n.+1%nat).-1.+1 a = int_iter f (- n.+1%nat).-1 (f a)
    rewrite int_pred_succ.
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f (- n.+1%nat).+1 a = int_iter f (- n.+1%nat) (f a)
int_iter f (- n.+1%nat) a = int_iter f (- n.+1%nat).-1 (f a)
    apply (ap f^-1).
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f (- n.+1%nat).+1 a = int_iter f (- n.+1%nat) (f a)
nat_iter n f^-1 a = f^-1 (nat_iter n f^-1 (f a))
    rhs_V exact IHn.
A: Type
f: A -> A
H: IsEquiv f
n: nat
a: A
IHn: int_iter f (- n.+1%nat).+1 a = int_iter f (- n.+1%nat) (f a)
nat_iter n f^-1 a = int_iter f (- n.+1%nat).+1 a
    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).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f n.-1 a = f^-1 (int_iter f n a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f n.-1 a = f^-1 (int_iter f n a)
  (* Convert the problem to be a problem about [f^-1] and [-n]. *)
  lhs_V exact (int_iter_neg f^-1 (n.-1) a).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f^-1 (- n.-1) a = f^-1 (int_iter f n a)
  rhs_V exact (ap f^-1 (int_iter_neg f^-1 n a)).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f^-1 (- n.-1) a = f^-1 (int_iter f^-1 (- n) a)
  (* Then [int_iter_succ_l] applies, after changing [- n.-1] to [(-n).+1]. *)
  rewrite int_neg_pred.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f^-1 (- n).+1 a = f^-1 (int_iter f^-1 (- n) a)
  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).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f n.-1 a = int_iter f n (f^-1 a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f n.-1 a = int_iter f n (f^-1 a)
  (* Convert the problem to be a problem about [f^-1] and [-n]. *)
  lhs_V exact (int_iter_neg f^-1 (n.-1) a).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f^-1 (- n.-1) a = int_iter f n (f^-1 a)
  rhs_V exact (int_iter_neg f^-1 n (f^-1 a)).
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f^-1 (- n.-1) a = int_iter f^-1 (- n) (f^-1 a)
  (* Then [int_iter_succ_r] applies, after changing [- n.-1] to [(-n).+1]. *)
  rewrite int_neg_pred.
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f^-1 (- n).+1 a = int_iter f^-1 (- n) (f^-1 a)
  apply int_iter_succ_r.
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.
A: Type
f: A -> A
H: IsEquiv f
m, n: Int
int_iter f (m + n) == int_iter f m o int_iter f n
Proof.
A: Type
f: A -> A
H: IsEquiv f
m, n: Int
int_iter f (m + n) == int_iter f m o int_iter f n
  intros a.
A: Type
f: A -> A
H: IsEquiv f
m, n: Int
a: A
int_iter f (m + n) a = int_iter f m (int_iter f n a)
  induction m as [|m|m].
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (0 + n) a = int_iter f 0 (int_iter f n a)
A: Type
f: A -> A
H: IsEquiv f
m: nat
n: Int
a: A
IHm: int_iter f (m + n) a = int_iter f m (int_iter f n a)
int_iter f (m.+1 + n) a = int_iter f m.+1 (int_iter f n a)
A: Type
f: A -> A
H: IsEquiv f
m: nat
n: Int
a: A
IHm: int_iter f (- m + n) a = int_iter f (- m) (int_iter f n a)
int_iter f ((- m).-1 + n) a = int_iter f (- m).-1 (int_iter f n a)
  -
A: Type
f: A -> A
H: IsEquiv f
n: Int
a: A
int_iter f (0 + n) a = int_iter f 0 (int_iter f n a) reflexivity.
  -
A: Type
f: A -> A
H: IsEquiv f
m: nat
n: Int
a: A
IHm: int_iter f (m + n) a = int_iter f m (int_iter f n a)
int_iter f (m.+1 + n) a = int_iter f m.+1 (int_iter f n a) rewrite int_add_succ_l.
A: Type
f: A -> A
H: IsEquiv f
m: nat
n: Int
a: A
IHm: int_iter f (m + n) a = int_iter f m (int_iter f n a)
int_iter f (m + n).+1 a = int_iter f m.+1 (int_iter f n a)
    rewrite 2 int_iter_succ_l.
A: Type
f: A -> A
H: IsEquiv f
m: nat
n: Int
a: A
IHm: int_iter f (m + n) a = int_iter f m (int_iter f n a)
f (int_iter f (m + n) a) = f (int_iter f m (int_iter f n a))
    f_ap.
  -
A: Type
f: A -> A
H: IsEquiv f
m: nat
n: Int
a: A
IHm: int_iter f (- m + n) a = int_iter f (- m) (int_iter f n a)
int_iter f ((- m).-1 + n) a = int_iter f (- m).-1 (int_iter f n a) rewrite int_add_pred_l.
A: Type
f: A -> A
H: IsEquiv f
m: nat
n: Int
a: A
IHm: int_iter f (- m + n) a = int_iter f (- m) (int_iter f n a)
int_iter f (- m + n).-1 a = int_iter f (- m).-1 (int_iter f n a)
    rewrite 2 int_iter_pred_l.
A: Type
f: A -> A
H: IsEquiv f
m: nat
n: Int
a: A
IHm: int_iter f (- m + n) a = int_iter f (- m) (int_iter f n a)
f^-1 (int_iter f (- m + n) a) = f^-1 (int_iter f (- m) (int_iter f n a))
    f_ap.
Defined.

(** 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).
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: 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.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: 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)
  induction n as [|n IHn|n IHn] in a |- *.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
a: A
g (int_iter f 0 a) = int_iter f' 0 (g a)
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f n a0) = int_iter f' n (g a0)
g (int_iter f n.+1 a) = int_iter f' n.+1 (g a)
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f (- n) a0) = int_iter f' (- n) (g a0)
g (int_iter f (- n).-1 a) = int_iter f' (- n).-1 (g a)
  -
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
a: A
g (int_iter f 0 a) = int_iter f' 0 (g a) reflexivity.
  -
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f n a0) = int_iter f' n (g a0)
g (int_iter f n.+1 a) = int_iter f' n.+1 (g a) rewrite 2 int_iter_succ_r.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f n a0) = int_iter f' n (g a0)
g (int_iter f n (f a)) = int_iter f' n (f' (g a))
    rewrite IHn.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f n a0) = int_iter f' n (g a0)
int_iter f' n (g (f a)) = int_iter f' n (f' (g a))
    f_ap.
  -
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f (- n) a0) = int_iter f' (- n) (g a0)
g (int_iter f (- n).-1 a) = int_iter f' (- n).-1 (g a) rewrite 2 int_iter_pred_r.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f (- n) a0) = int_iter f' (- n) (g a0)
g (int_iter f (- n) (f^-1 a)) = int_iter f' (- n) (f'^-1 (g a))
    rewrite IHn.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f (- n) a0) = int_iter f' (- n) (g a0)
int_iter f' (- n) (g (f^-1 a)) = int_iter f' (- n) (f'^-1 (g a))
    f_ap.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f (- n) a0) = int_iter f' (- n) (g a0)
g (f^-1 a) = f'^-1 (g a)
    apply moveL_equiv_V.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f (- n) a0) = int_iter f' (- n) (g a0)
f' (g (f^-1 a)) = g a
    lhs_V napply p.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f (- n) a0) = int_iter f' (- n) (g a0)
g (f (f^-1 a)) = g a
    f_ap.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
n: nat
a: A
IHn: forall a0 : A, g (int_iter f (- n) a0) = int_iter f' (- n) (g a0)
f (f^-1 a) = a
    apply eisretr.
Defined.

(** In particular, homotopic maps have homotopic iterations. *)
Definition int_iter_homotopic (n : Int) {A} (f f' : A -> A) `{!IsEquiv f} `{!IsEquiv f'}
  (h : f == f')
  : int_iter f n == int_iter f' n
  := int_iter_commute_map f f' idmap h n.

(** [int_iter f n x] doesn't depend on the proof that [f] is an equivalence. *)
Definition int_iter_agree (n : Int) {A} (f : A -> A) {ief ief' : IsEquiv f}
  : forall x, @int_iter A f ief n x = @int_iter A f ief' n x
  := int_iter_homotopic n f f (fun _ => idpath).

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).
n: Int
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x : A, P x -> P (f x)
Ppred: forall x : A, P x -> P (f^-1 x)
forall x : A, P x -> P (int_iter f n x)
Proof.
n: Int
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x : A, P x -> P (f x)
Ppred: forall x : A, P x -> P (f^-1 x)
forall x : A, P x -> P (int_iter f n x)
  induction n as [|n IHn|n IHn]; intro x.
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x0 : A, P x0 -> P (f x0)
Ppred: forall x0 : A, P x0 -> P (f^-1 x0)
x: A
P x -> P (int_iter f 0 x)
n: nat
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x0 : A, P x0 -> P (f x0)
Ppred: forall x0 : A, P x0 -> P (f^-1 x0)
IHn: forall x0 : A, P x0 -> P (int_iter f n x0)
x: A
P x -> P (int_iter f n.+1 x)
n: nat
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x0 : A, P x0 -> P (f x0)
Ppred: forall x0 : A, P x0 -> P (f^-1 x0)
IHn: forall x0 : A, P x0 -> P (int_iter f (- n) x0)
x: A
P x -> P (int_iter f (- n).-1 x)
  -
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x0 : A, P x0 -> P (f x0)
Ppred: forall x0 : A, P x0 -> P (f^-1 x0)
x: A
P x -> P (int_iter f 0 x) exact idmap.
  -
n: nat
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x0 : A, P x0 -> P (f x0)
Ppred: forall x0 : A, P x0 -> P (f^-1 x0)
IHn: forall x0 : A, P x0 -> P (int_iter f n x0)
x: A
P x -> P (int_iter f n.+1 x) intro H.
n: nat
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x0 : A, P x0 -> P (f x0)
Ppred: forall x0 : A, P x0 -> P (f^-1 x0)
IHn: forall x0 : A, P x0 -> P (int_iter f n x0)
x: A
H: P x
P (int_iter f n.+1 x)
    rewrite int_iter_succ_l.
n: nat
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x0 : A, P x0 -> P (f x0)
Ppred: forall x0 : A, P x0 -> P (f^-1 x0)
IHn: forall x0 : A, P x0 -> P (int_iter f n x0)
x: A
H: P x
P (f (int_iter f n x))
    apply Psucc, IHn, H.
  -
n: nat
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x0 : A, P x0 -> P (f x0)
Ppred: forall x0 : A, P x0 -> P (f^-1 x0)
IHn: forall x0 : A, P x0 -> P (int_iter f (- n) x0)
x: A
P x -> P (int_iter f (- n).-1 x) intro H.
n: nat
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x0 : A, P x0 -> P (f x0)
Ppred: forall x0 : A, P x0 -> P (f^-1 x0)
IHn: forall x0 : A, P x0 -> P (int_iter f (- n) x0)
x: A
H: P x
P (int_iter f (- n).-1 x)
    rewrite int_iter_pred_l.
n: nat
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall x0 : A, P x0 -> P (f x0)
Ppred: forall x0 : A, P x0 -> P (f^-1 x0)
IHn: forall x0 : A, P x0 -> P (int_iter f (- n) x0)
x: A
H: P x
P (f^-1 (int_iter f (- n) x))
    apply Ppred, IHn, H.
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.
A: Type
x: A
p: x = x
z: Int
loopexp p z.+1 = p @ loopexp p z
Proof.
A: Type
x: A
p: x = x
z: Int
loopexp p z.+1 = p @ loopexp p z
  lhs napply loopexp_succ_r.
A: Type
x: A
p: x = x
z: Int
loopexp p z @ p = p @ loopexp p z
  induction z as [|z|z].
A: Type
x: A
p: x = x
loopexp p 0 @ p = p @ loopexp p 0
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p z @ p = p @ loopexp p z
loopexp p z.+1 @ p = p @ loopexp p z.+1
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p (- z) @ p = p @ loopexp p (- z)
loopexp p (- z).-1 @ p = p @ loopexp p (- z).-1
  -
A: Type
x: A
p: x = x
loopexp p 0 @ p = p @ loopexp p 0 napply concat_1p_p1.
  -
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p z @ p = p @ loopexp p z
loopexp p z.+1 @ p = p @ loopexp p z.+1 rewrite loopexp_succ_r.
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p z @ p = p @ loopexp p z
(loopexp p z @ p) @ p = p @ (loopexp p z @ p)
    rhs napply concat_p_pp.
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p z @ p = p @ loopexp p z
(loopexp p z @ p) @ p = (p @ loopexp p z) @ p
    f_ap.
  -
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p (- z) @ p = p @ loopexp p (- z)
loopexp p (- z).-1 @ p = p @ loopexp p (- z).-1 rewrite loopexp_pred_r.
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p (- z) @ p = p @ loopexp p (- z)
(loopexp p (- z) @ p^) @ p = p @ (loopexp p (- z) @ p^)
    lhs napply concat_pV_p.
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p (- z) @ p = p @ loopexp p (- z)
loopexp p (- z) = p @ (loopexp p (- z) @ p^)
    rhs napply concat_p_pp.
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p (- z) @ p = p @ loopexp p (- z)
loopexp p (- z) = (p @ loopexp p (- z)) @ p^
    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.
A: Type
x: A
p: x = x
z: Int
loopexp p z.-1 = p^ @ loopexp p z
Proof.
A: Type
x: A
p: x = x
z: Int
loopexp p z.-1 = p^ @ loopexp p z
  rewrite loopexp_pred_r.
A: Type
x: A
p: x = x
z: Int
loopexp p z @ p^ = p^ @ loopexp p z
  induction z as [|z|z].
A: Type
x: A
p: x = x
loopexp p 0 @ p^ = p^ @ loopexp p 0
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p z @ p^ = p^ @ loopexp p z
loopexp p z.+1 @ p^ = p^ @ loopexp p z.+1
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p (- z) @ p^ = p^ @ loopexp p (- z)
loopexp p (- z).-1 @ p^ = p^ @ loopexp p (- z).-1
  -
A: Type
x: A
p: x = x
loopexp p 0 @ p^ = p^ @ loopexp p 0 exact (concat_1p _ @ (concat_p1 _)^).
  -
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p z @ p^ = p^ @ loopexp p z
loopexp p z.+1 @ p^ = p^ @ loopexp p z.+1 rewrite loopexp_succ_r.
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p z @ p^ = p^ @ loopexp p z
(loopexp p z @ p) @ p^ = p^ @ (loopexp p z @ p)
    lhs napply concat_pp_V.
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p z @ p^ = p^ @ loopexp p z
loopexp p z = p^ @ (loopexp p z @ p)
    rhs napply concat_p_pp.
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p z @ p^ = p^ @ loopexp p z
loopexp p z = (p^ @ loopexp p z) @ p
    by apply moveL_pM.
  -
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p (- z) @ p^ = p^ @ loopexp p (- z)
loopexp p (- z).-1 @ p^ = p^ @ loopexp p (- z).-1 rewrite loopexp_pred_r.
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p (- z) @ p^ = p^ @ loopexp p (- z)
(loopexp p (- z) @ p^) @ p^ = p^ @ (loopexp p (- z) @ p^)
    rhs napply concat_p_pp.
A: Type
x: A
p: x = x
z: nat
IHz: loopexp p (- z) @ p^ = p^ @ loopexp p (- z)
(loopexp p (- z) @ p^) @ p^ = (p^ @ loopexp p (- z)) @ p^
    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.
A, B: Type
f: A -> B
x: A
p: x = x
z: Int
ap f (loopexp p z) = loopexp (ap f p) z
Proof.
A, B: Type
f: A -> B
x: A
p: x = x
z: Int
ap f (loopexp p z) = loopexp (ap f p) z
  napply int_iter_commute_map.
A, B: Type
f: A -> B
x: A
p: x = x
z: Int
(fun x0 : x = x => ap f (equiv_concat_r p x x0)) ==
(fun x0 : x = x => equiv_concat_r (ap f p) (f x) (ap f x0))
  intro q; apply ap_pp.
Defined.

Definition loopexp_add {A : Type} {x : A} (p : x = x) m n
  : loopexp p (m + n) = loopexp p m @ loopexp p n.
A: Type
x: A
p: x = x
m, n: Int
loopexp p (m + n) = loopexp p m @ loopexp p n
Proof.
A: Type
x: A
p: x = x
m, n: Int
loopexp p (m + n) = loopexp p m @ loopexp p n
  induction m as [|m|m].
A: Type
x: A
p: x = x
n: Int
loopexp p (0 + n) = loopexp p 0 @ loopexp p n
A: Type
x: A
p: x = x
m: nat
n: Int
IHm: loopexp p (m + n) = loopexp p m @ loopexp p n
loopexp p (m.+1 + n) = loopexp p m.+1 @ loopexp p n
A: Type
x: A
p: x = x
m: nat
n: Int
IHm: loopexp p (- m + n) = loopexp p (- m) @ loopexp p n
loopexp p ((- m).-1 + n) = loopexp p (- m).-1 @ loopexp p n
  -
A: Type
x: A
p: x = x
n: Int
loopexp p (0 + n) = loopexp p 0 @ loopexp p n symmetry; apply concat_1p.
  -
A: Type
x: A
p: x = x
m: nat
n: Int
IHm: loopexp p (m + n) = loopexp p m @ loopexp p n
loopexp p (m.+1 + n) = loopexp p m.+1 @ loopexp p n rewrite int_add_succ_l.
A: Type
x: A
p: x = x
m: nat
n: Int
IHm: loopexp p (m + n) = loopexp p m @ loopexp p n
loopexp p (m + n).+1 = loopexp p m.+1 @ loopexp p n
    rewrite 2 loopexp_succ_l.
A: Type
x: A
p: x = x
m: nat
n: Int
IHm: loopexp p (m + n) = loopexp p m @ loopexp p n
p @ loopexp p (m + n) = (p @ loopexp p m) @ loopexp p n
    by rewrite IHm, concat_p_pp.
  -
A: Type
x: A
p: x = x
m: nat
n: Int
IHm: loopexp p (- m + n) = loopexp p (- m) @ loopexp p n
loopexp p ((- m).-1 + n) = loopexp p (- m).-1 @ loopexp p n rewrite int_add_pred_l.
A: Type
x: A
p: x = x
m: nat
n: Int
IHm: loopexp p (- m + n) = loopexp p (- m) @ loopexp p n
loopexp p (- m + n).-1 = loopexp p (- m).-1 @ loopexp p n
    rewrite 2 loopexp_pred_l.
A: Type
x: A
p: x = x
m: nat
n: Int
IHm: loopexp p (- m + n) = loopexp p (- m) @ loopexp p n
p^ @ loopexp p (- m + n) = (p^ @ loopexp p (- m)) @ loopexp p n
    by rewrite IHm, concat_p_pp.
Defined.

(** Under univalence, exponentiation of loops corresponds to iteration of auto-equivalences. *)

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.
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.
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
  refine (int_iter_commute_map _ _ (fun p => equiv_path A A p a) _ _ _).
A: Type
p: A = A
z: Int
a: A
(fun x : A = A => equiv_path A A (equiv_concat_r p A x) a) ==
(fun x : A = A => equiv_path A A p (equiv_path A A x a))
  intro q; cbn.
A: Type
p: A = A
z: Int
a: A
q: A = A
transport idmap (q @ p) a = transport idmap p (transport idmap q a)
  napply transport_pp.
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.
H: Univalence
A: Type
f: A <~> A
z: Int
a: A
transport idmap (loopexp (path_universe f) z) a = int_iter f z a
Proof.
H: Univalence
A: Type
f: A <~> A
z: Int
a: A
transport idmap (loopexp (path_universe f) z) a = int_iter f z a
  revert f.
H: Univalence
A: Type
z: Int
a: A
forall f : A <~> A,
transport idmap (loopexp (path_universe f) z) a = int_iter f z a equiv_intro (equiv_path A A) p.
H: Univalence
A: Type
z: Int
a: A
p: A = A
transport idmap (loopexp (path_universe (equiv_path A A p)) z) a =
int_iter (equiv_path A A p) z a
  refine (_ @ equiv_path_loopexp p z a).
H: Univalence
A: Type
z: Int
a: A
p: A = A
transport idmap (loopexp (path_universe (equiv_path A A p)) z) a =
equiv_path A A (loopexp p z) a
  refine (ap (fun q => equiv_path A A (loopexp q z) a) _).
H: Univalence
A: Type
z: Int
a: A
p: A = A
path_universe (equiv_path A A p) = p
  apply eissect.
Defined.

(** ** Converting between integers and naturals *)

(** [int_of_nat] preserves successors. *)
Definition int_nat_succ (n : nat)
  : (n.+1)%int = (n.+1)%nat :> Int.
n: nat
n.+1 = n.+1%nat
Proof.
n: nat
n.+1 = n.+1%nat
  by induction n.
Defined.

(** [int_of_nat] preserves addition. Hence is a monoid homomorphism. *)
Definition int_nat_add (n m : nat)
  : (n + m)%int = (n + m)%nat :> Int.
n, m: nat
n + m = (n + m)%nat
Proof.
n, m: nat
n + m = (n + m)%nat
  induction n as [|n IHn].
m: nat
0%nat + m = (0 + m)%nat
n, m: nat
IHn: n + m = (n + m)%nat
n.+1%nat + m = (n.+1 + m)%nat
  -
m: nat
0%nat + m = (0 + m)%nat reflexivity.
  -
n, m: nat
IHn: n + m = (n + m)%nat
n.+1%nat + m = (n.+1 + m)%nat rewrite <- 2 int_nat_succ.
n, m: nat
IHn: n + m = (n + m)%nat
n.+1 + m = (nat_iter n S m).+1
    rewrite int_add_succ_l.
n, m: nat
IHn: n + m = (n + m)%nat
(n + m).+1 = (nat_iter n S m).+1
    exact (ap _ IHn).
Defined.

(** [int_of_nat] preserves subtraction when not truncated. *)
Definition int_nat_sub (n m : nat)
  : (m <= n)%nat -> (n - m)%int = (n - m)%nat :> Int.
n, m: nat
(m <= n)%nat -> n - m = (n - m)%nat
Proof.
n, m: nat
(m <= n)%nat -> n - m = (n - m)%nat
  intros H.
n, m: nat
H: (m <= n)%nat
n - m = (n - m)%nat
  induction H as [|n H IHn].
m: nat
m + - m = (m - m)%nat
m, n: nat
H: (m <= n)%nat
IHn: n + - m = (n - m)%nat
n.+1%nat + - m = (n.+1 - m)%nat
  -
m: nat
m + - m = (m - m)%nat lhs napply int_add_neg_r.
m: nat
0 = (m - m)%nat
    by rewrite nat_sub_cancel.
  -
m, n: nat
H: (m <= n)%nat
IHn: n + - m = (n - m)%nat
n.+1%nat + - m = (n.+1 - m)%nat rewrite nat_sub_succ_l; only 2: exact _.
m, n: nat
H: (m <= n)%nat
IHn: n + - m = (n - m)%nat
n.+1%nat + - m = (n - m).+1%nat
    rewrite <- 2 int_nat_succ.
m, n: nat
H: (m <= n)%nat
IHn: n + - m = (n - m)%nat
n.+1 + - m = (n - m)%nat.+1
    rewrite int_add_succ_l.
m, n: nat
H: (m <= n)%nat
IHn: n + - m = (n - m)%nat
(n + - m).+1 = (n - m)%nat.+1
    exact (ap _ IHn).
Defined.

(** [int_of_nat] preserves multiplication. This makes [int_of_nat] a semiring homomorphism. *)
Definition int_nat_mul (n m : nat)
  :  (n * m)%int = (n * m)%nat :> Int.
n, m: nat
n * m = (n * m)%nat
Proof.
n, m: nat
n * m = (n * m)%nat
  induction n as [|n IHn].
m: nat
0%nat * m = (0 * m)%nat
n, m: nat
IHn: n * m = (n * m)%nat
n.+1%nat * m = (n.+1 * m)%nat
  -
m: nat
0%nat * m = (0 * m)%nat reflexivity.
  -
n, m: nat
IHn: n * m = (n * m)%nat
n.+1%nat * m = (n.+1 * m)%nat rewrite <- int_nat_succ.
n, m: nat
IHn: n * m = (n * m)%nat
n.+1 * m = (n.+1 * m)%nat
    rewrite int_mul_succ_l.
n, m: nat
IHn: n * m = (n * m)%nat
m + n * m = (n.+1 * m)%nat
    rewrite nat_mul_succ_l.
n, m: nat
IHn: n * m = (n * m)%nat
m + n * m = (m + n * m)%nat
    rhs_V napply int_nat_add.
n, m: nat
IHn: n * m = (n * m)%nat
m + n * m = m + (n * m)%nat
    exact (ap _ IHn).
Defined.