Int.v

Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
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 y : Int, 0%nat.+1 + y = (0%nat + y).+1
0%nat.+1.+1 + y = (0%nat.+1 + y).+1
x: nat
y: Int
IHx: forall y : Int, x.+1%nat.+1 + y = (x.+1%nat + y).+1
x.+1%nat.+1.+1 + y = (x.+1%nat.+1 + y).+1
y: Int
IHx: forall y : Int, (- 0%nat).+1 + y = (- 0%nat + y).+1
(- 0%nat).-1.+1 + y = ((- 0%nat).-1 + y).+1
x: nat
y: Int
IHx: forall y : Int, (- x.+1%nat).+1 + y = (- x.+1%nat + y).+1
(- x.+1%nat).-1.+1 + y = ((- x.+1%nat).-1 + y).+1
  1-3: reflexivity.y: Int
IHx: forall y : Int, (- 0%nat).+1 + y = (- 0%nat + y).+1
(- 0%nat).-1.+1 + y = ((- 0%nat).-1 + y).+1
x: nat
y: Int
IHx: forall y : Int, (- x.+1%nat).+1 + y = (- x.+1%nat + y).+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 y : Int, 0%nat.-1 + y = (0%nat + y).-1
0%nat.+1.-1 + y = (0%nat.+1 + y).-1
x: nat
y: Int
IHx: forall y : Int, x.+1%nat.-1 + y = (x.+1%nat + y).-1
x.+1%nat.+1.-1 + y = (x.+1%nat.+1 + y).-1
y: Int
IHx: forall y : Int, (- 0%nat).-1 + y = (- 0%nat + y).-1
(- 0%nat).-1.-1 + y = ((- 0%nat).-1 + y).-1
x: nat
y: Int
IHx: forall y : Int, (- x.+1%nat).-1 + y = (- x.+1%nat + y).-1
(- x.+1%nat).-1.-1 + y = ((- x.+1%nat).-1 + y).-1
  1,4,5: reflexivity.y: Int
IHx: forall y : Int, 0%nat.-1 + y = (0%nat + y).-1
0%nat.+1.-1 + y = (0%nat.+1 + y).-1
x: nat
y: Int
IHx: forall y : Int, x.+1%nat.-1 + y = (x.+1%nat + y).-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 y : Int, x + y.+1 = (x + y).+1
x.+1 + y.+1 = (x.+1 + y).+1
y: Int
IHx: forall y : Int, - 0%nat + y.+1 = (- 0%nat + y).+1
(- 0%nat).-1 + y.+1 = ((- 0%nat).-1 + y).+1
n: nat
y: Int
IHx: forall y : Int, - n.+1%nat + y.+1 = (- n.+1%nat + y).+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 y : Int, x + y.+1 = (x + y).+1
x.+1 + y.+1 = (x.+1 + y).+1 by rewrite 2 int_add_succ_l, IHx.
  -y: Int
IHx: forall y : Int, - 0%nat + y.+1 = (- 0%nat + y).+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 y : Int, - n.+1%nat + y.+1 = (- n.+1%nat + y).+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 y : Int, - n.+1%nat + y.+1 = (- n.+1%nat + y).+1
(- n.+1%nat).-1 + y.+1 = ((- n.+1%nat).-1 + y).+1
    rewrite int_add_pred_l.n: nat
y: Int
IHx: forall y : Int, - n.+1%nat + y.+1 = (- n.+1%nat + y).+1
(- n.+1%nat + y.+1).-1 = ((- n.+1%nat).-1 + y).+1
    rewrite IHx.n: nat
y: Int
IHx: forall y : Int, - n.+1%nat + y.+1 = (- n.+1%nat + y).+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 y : Int, - n.+1%nat + y.+1 = (- n.+1%nat + y).+1
((- n.+1%nat).+1 + y).-1 = (- n.+1%nat).-1.+1 + y
    rewrite <- int_add_pred_l.n: nat
y: Int
IHx: forall y : Int, - n.+1%nat + y.+1 = (- n.+1%nat + y).+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 y : Int, x + y.-1 = (x + y).-1
x.+1 + y.-1 = (x.+1 + y).-1
y: Int
IHx: forall y : Int, - 0%nat + y.-1 = (- 0%nat + y).-1
(- 0%nat).-1 + y.-1 = ((- 0%nat).-1 + y).-1
n: nat
y: Int
IHx: forall y : Int, - n.+1%nat + y.-1 = (- n.+1%nat + y).-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 y : Int, x + y.-1 = (x + y).-1
x.+1 + y.-1 = (x.+1 + y).-1 rewrite 2 int_add_succ_l.x: nat
y: Int
IHx: forall y : Int, x + y.-1 = (x + y).-1
(x + y.-1).+1 = (x + y).+1.-1
    rewrite IHx.x: nat
y: Int
IHx: forall y : Int, x + y.-1 = (x + y).-1
(x + y).-1.+1 = (x + y).+1.-1
    by rewrite int_pred_succ, int_succ_pred.
  -y: Int
IHx: forall y : Int, - 0%nat + y.-1 = (- 0%nat + y).-1
(- 0%nat).-1 + y.-1 = ((- 0%nat).-1 + y).-1 reflexivity.
  -n: nat
y: Int
IHx: forall y : Int, - n.+1%nat + y.-1 = (- n.+1%nat + y).-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 y : Int, - n.+1%nat + y.-1 = (- n.+1%nat + y).-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 x : Int, x + y = y + x
x + y.+1 = y.+1 + x
x: Int
y: nat
IHy: forall x : Int, x + - y = - y + x
x + (- y).-1 = (- y).-1 + x
  -x: Int
x + 0 = 0 + x apply int_add_0_r.
  -x: Int
y: nat
IHy: forall x : Int, x + y = y + x
x + y.+1 = y.+1 + x rewrite int_add_succ_l.x: Int
y: nat
IHy: forall x : Int, x + y = y + x
x + y.+1 = (y + x).+1
    rewrite <- IHy.x: Int
y: nat
IHy: forall x : Int, x + y = y + x
x + y.+1 = (x + y).+1
    by rewrite int_add_succ_r.
  -x: Int
y: nat
IHy: forall x : Int, x + - y = - y + x
x + (- y).-1 = (- y).-1 + x rewrite int_add_pred_r.x: Int
y: nat
IHy: forall x : Int, x + - y = - y + x
(x + - y).-1 = (- y).-1 + x
    rewrite int_add_pred_l.x: Int
y: nat
IHy: forall x : Int, x + - y = - y + x
(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 y z : Int, x + (y + z) = x + y + z
x.+1 + (y + z) = x.+1 + y + z
x: nat
y, z: Int
IHx: forall y z : Int, - x + (y + z) = - x + y + z
(- 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 y z : Int, x + (y + z) = x + y + z
x.+1 + (y + z) = x.+1 + y + z by rewrite !int_add_succ_l, IHx.
  -x: nat
y, z: Int
IHx: forall y z : Int, - x + (y + z) = - x + y + z
(- 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 y : Int, - (x + y) = - x + - y
- (x.+1 + y) = - x.+1 + - y
x: nat
y: Int
IHx: forall y : Int, - (- x + y) = - - x + - y
- ((- x).-1 + y) = - (- x).-1 + - y
  -y: Int
- (0 + y) = - 0 + - y reflexivity.
  -x: nat
y: Int
IHx: forall y : Int, - (x + y) = - x + - y
- (x.+1 + y) = - x.+1 + - y rewrite int_add_succ_l.x: nat
y: Int
IHx: forall y : Int, - (x + y) = - x + - y
- (x + y).+1 = - x.+1 + - y
    rewrite 2 int_neg_succ.x: nat
y: Int
IHx: forall y : Int, - (x + y) = - x + - y
(- (x + y)).-1 = (- x).-1 + - y
    rewrite int_add_pred_l.x: nat
y: Int
IHx: forall y : Int, - (x + y) = - x + - y
(- (x + y)).-1 = (- x + - y).-1
    f_ap.
  -x: nat
y: Int
IHx: forall y : Int, - (- x + y) = - - x + - y
- ((- x).-1 + y) = - (- x).-1 + - y rewrite int_neg_pred.x: nat
y: Int
IHx: forall y : Int, - (- x + y) = - - x + - y
- ((- x).-1 + y) = (- - x).+1 + - y
    rewrite int_add_succ_l.x: nat
y: Int
IHx: forall y : Int, - (- x + y) = - - x + - y
- ((- x).-1 + y) = (- - x + - y).+1
    rewrite int_add_pred_l.x: nat
y: Int
IHx: forall y : Int, - (- x + y) = - - x + - y
- (- x + y).-1 = (- - x + - y).+1
    rewrite int_neg_pred.x: nat
y: Int
IHx: forall y : Int, - (- x + y) = - - x + - y
(- (- 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 y : Int, 0%nat.+1 * y = y + 0%nat * y
0%nat.+1.+1 * y = y + 0%nat.+1 * y
x: nat
y: Int
IHx: forall y : Int, x.+1%nat.+1 * y = y + x.+1%nat * y
x.+1%nat.+1.+1 * y = y + x.+1%nat.+1 * y
y: Int
IHx: forall y : Int, (- 0%nat).+1 * y = y + - 0%nat * y
(- 0%nat).-1.+1 * y = y + (- 0%nat).-1 * y
n: nat
y: Int
IHx: forall y : Int, (- n.+1%nat).+1 * y = y + - n.+1%nat * y
(- 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 y : Int, 0%nat.+1 * y = y + 0%nat * y
0%nat.+1.+1 * y = y + 0%nat.+1 * y reflexivity.
  -x: nat
y: Int
IHx: forall y : Int, x.+1%nat.+1 * y = y + x.+1%nat * y
x.+1%nat.+1.+1 * y = y + x.+1%nat.+1 * y reflexivity.
  -y: Int
IHx: forall y : Int, (- 0%nat).+1 * y = y + - 0%nat * y
(- 0%nat).-1.+1 * y = y + (- 0%nat).-1 * y cbn.y: Int
IHx: forall y : Int, (- 0%nat).+1 * y = y + - 0%nat * y
0 = y + (- y + 0)
    rewrite int_add_0_r.y: Int
IHx: forall y : Int, (- 0%nat).+1 * y = y + - 0%nat * y
0 = y + - y
    by rewrite int_add_neg_r.
  -n: nat
y: Int
IHx: forall y : Int, (- n.+1%nat).+1 * y = y + - n.+1%nat * y
(- n.+1%nat).-1.+1 * y = y + (- n.+1%nat).-1 * y rewrite int_pred_succ.n: nat
y: Int
IHx: forall y : Int, (- n.+1%nat).+1 * y = y + - n.+1%nat * y
- n.+1%nat * y = y + (- n.+1%nat).-1 * y
    cbn.n: nat
y: Int
IHx: forall y : Int, (- n.+1%nat).+1 * y = y + - n.+1%nat * y
nat_rect (fun _ : nat => Int -> Int)
  (fun y : Int => - y + 0)
  (fun (_ : nat) (IHx : Int -> Int) (y : Int) =>
   - y + IHx y) n y =
y +
(- y +
 nat_rect (fun _ : nat => Int -> Int)
   (fun y : Int => - y + 0)
   (fun (_ : nat) (IHx : Int -> Int) (y : Int) =>
    - y + IHx y) n y)
    rewrite int_add_assoc.n: nat
y: Int
IHx: forall y : Int, (- n.+1%nat).+1 * y = y + - n.+1%nat * y
nat_rect (fun _ : nat => Int -> Int)
  (fun y : Int => - y + 0)
  (fun (_ : nat) (IHx : Int -> Int) (y : Int) =>
   - y + IHx y) n y =
y + - y +
nat_rect (fun _ : nat => Int -> Int)
  (fun y : Int => - y + 0)
  (fun (_ : nat) (IHx : Int -> Int) (y : Int) =>
   - y + IHx y) n y
    rewrite int_add_neg_r.n: nat
y: Int
IHx: forall y : Int, (- n.+1%nat).+1 * y = y + - n.+1%nat * y
nat_rect (fun _ : nat => Int -> Int)
  (fun y : Int => - y + 0)
  (fun (_ : nat) (IHx : Int -> Int) (y : Int) =>
   - y + IHx y) n y =
0 +
nat_rect (fun _ : nat => Int -> Int)
  (fun y : Int => - y + 0)
  (fun (_ : nat) (IHx : Int -> Int) (y : Int) =>
   - y + IHx y) 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 y : Int, x.-1 * y = - y + x * y
x.+1.-1 * y = - y + x.+1 * y
y: Int
IHx: forall y : Int, (- 0%nat).-1 * y = - y + - 0%nat * y
(- 0%nat).-1.-1 * y = - y + (- 0%nat).-1 * y
n: nat
y: Int
IHx: forall y : Int, (- n.+1%nat).-1 * y = - y + - n.+1%nat * y
(- 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 y : Int, x.-1 * y = - y + x * y
x.+1.-1 * y = - y + x.+1 * y rewrite int_mul_succ_l.x: nat
y: Int
IHx: forall y : Int, x.-1 * y = - y + x * y
x.+1.-1 * y = - y + (y + x * y)
    rewrite int_succ_pred.x: nat
y: Int
IHx: forall y : Int, x.-1 * y = - y + x * y
x * y = - y + (y + x * y)
    rewrite int_add_assoc.x: nat
y: Int
IHx: forall y : Int, x.-1 * y = - y + x * y
x * y = - y + y + x * y
    by rewrite int_add_neg_l.
  -y: Int
IHx: forall y : Int, (- 0%nat).-1 * y = - y + - 0%nat * y
(- 0%nat).-1.-1 * y = - y + (- 0%nat).-1 * y reflexivity.
  -n: nat
y: Int
IHx: forall y : Int, (- n.+1%nat).-1 * y = - y + - n.+1%nat * y
(- 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 y : Int, - x * y = - (x * y)
- x.+1 * y = - (x.+1 * y)
x: nat
y: Int
IHx: forall y : Int, - - x * y = - (- x * y)
- (- x).-1 * y = - ((- x).-1 * y)
  -y: Int
- 0 * y = - (0 * y) reflexivity.
  -x: nat
y: Int
IHx: forall y : Int, - x * y = - (x * y)
- x.+1 * y = - (x.+1 * y) rewrite int_neg_succ.x: nat
y: Int
IHx: forall y : Int, - x * y = - (x * y)
(- x).-1 * y = - (x.+1 * y)
    rewrite int_mul_pred_l.x: nat
y: Int
IHx: forall y : Int, - x * y = - (x * y)
- y + - x * y = - (x.+1 * y)
    rewrite int_mul_succ_l.x: nat
y: Int
IHx: forall y : Int, - x * y = - (x * y)
- y + - x * y = - (y + x * y)
    rewrite int_neg_add.x: nat
y: Int
IHx: forall y : Int, - x * y = - (x * y)
- y + - x * y = - y + - (x * y)
    by rewrite IHx.
  -x: nat
y: Int
IHx: forall y : Int, - - x * y = - (- x * y)
- (- x).-1 * y = - ((- x).-1 * y) rewrite int_neg_pred.x: nat
y: Int
IHx: forall y : Int, - - x * y = - (- x * y)
(- - x).+1 * y = - ((- x).-1 * y)
    rewrite int_mul_succ_l.x: nat
y: Int
IHx: forall y : Int, - - x * y = - (- x * y)
y + - - x * y = - ((- x).-1 * y)
    rewrite int_mul_pred_l.x: nat
y: Int
IHx: forall y : Int, - - x * y = - (- x * y)
y + - - x * y = - (- y + - x * y)
    rewrite int_neg_add.x: nat
y: Int
IHx: forall y : Int, - - x * y = - (- x * y)
y + - - x * y = - - y + - (- x * y)
    rewrite IHx.x: nat
y: Int
IHx: forall y : Int, - - x * y = - (- x * y)
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 y : Int, x * y.+1 = x + x * y
x.+1 * y.+1 = x.+1 + x.+1 * y
x: nat
y: Int
IHx: forall y : Int, - x * y.+1 = - x + - x * y
(- x).-1 * y.+1 = (- x).-1 + (- x).-1 * y
  -y: Int
0 * y.+1 = 0 + 0 * y reflexivity.
  -x: nat
y: Int
IHx: forall y : Int, x * y.+1 = x + x * y
x.+1 * y.+1 = x.+1 + x.+1 * y rewrite 2 int_mul_succ_l.x: nat
y: Int
IHx: forall y : Int, x * y.+1 = x + x * y
y.+1 + x * y.+1 = x.+1 + (y + x * y)
    rewrite 2 int_add_succ_l.x: nat
y: Int
IHx: forall y : Int, x * y.+1 = x + x * y
(y + x * y.+1).+1 = (x + (y + x * y)).+1
    f_ap.x: nat
y: Int
IHx: forall y : Int, x * y.+1 = x + x * y
y + x * y.+1 = x + (y + x * y)
    rewrite IHx.x: nat
y: Int
IHx: forall y : Int, x * y.+1 = x + x * y
y + (x + x * y) = x + (y + x * y)
    rewrite !int_add_assoc; f_ap.x: nat
y: Int
IHx: forall y : Int, x * y.+1 = x + x * y
y + x = x + y
    by rewrite int_add_comm.
  -x: nat
y: Int
IHx: forall y : Int, - x * y.+1 = - x + - x * y
(- x).-1 * y.+1 = (- x).-1 + (- x).-1 * y rewrite 2 int_mul_pred_l.x: nat
y: Int
IHx: forall y : Int, - x * y.+1 = - x + - x * y
- y.+1 + - x * y.+1 = (- x).-1 + (- y + - x * y)
    rewrite int_neg_succ.x: nat
y: Int
IHx: forall y : Int, - x * y.+1 = - x + - x * y
(- y).-1 + - x * y.+1 = (- x).-1 + (- y + - x * y)
    rewrite int_mul_neg_l.x: nat
y: Int
IHx: forall y : Int, - x * y.+1 = - x + - x * y
(- y).-1 + - (x * y.+1) = (- x).-1 + (- y + - x * y)
    rewrite 2 int_add_pred_l.x: nat
y: Int
IHx: forall y : Int, - x * y.+1 = - x + - x * y
(- y + - (x * y.+1)).-1 = (- x + (- y + - x * y)).-1
    f_ap.x: nat
y: Int
IHx: forall y : Int, - x * y.+1 = - x + - x * y
- y + - (x * y.+1) = - x + (- y + - x * y)
    rewrite <- int_mul_neg_l.x: nat
y: Int
IHx: forall y : Int, - x * y.+1 = - x + - x * y
- y + - x * y.+1 = - x + (- y + - x * y)
    rewrite IHx.x: nat
y: Int
IHx: forall y : Int, - x * y.+1 = - x + - x * y
- y + (- x + - x * y) = - x + (- y + - x * y)
    rewrite !int_add_assoc; f_ap.x: nat
y: Int
IHx: forall y : Int, - x * y.+1 = - x + - x * y
- 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 y : Int, x * y.-1 = - x + x * y
x.+1 * y.-1 = - x.+1 + x.+1 * y
x: nat
y: Int
IHx: forall y : Int, - x * y.-1 = - - x + - x * y
(- x).-1 * y.-1 = - (- x).-1 + (- x).-1 * y
  -y: Int
0 * y.-1 = - 0 + 0 * y reflexivity.
  -x: nat
y: Int
IHx: forall y : Int, x * y.-1 = - x + x * y
x.+1 * y.-1 = - x.+1 + x.+1 * y rewrite 2 int_mul_succ_l.x: nat
y: Int
IHx: forall y : Int, x * y.-1 = - x + x * y
y.-1 + x * y.-1 = - x.+1 + (y + x * y)
    rewrite IHx.x: nat
y: Int
IHx: forall y : Int, x * y.-1 = - x + x * y
y.-1 + (- x + x * y) = - x.+1 + (y + x * y)
    rewrite !int_add_assoc; f_ap.x: nat
y: Int
IHx: forall y : Int, x * y.-1 = - x + x * y
y.-1 + - x = - x.+1 + y
    rewrite <- (int_neg_neg y.-1).x: nat
y: Int
IHx: forall y : Int, x * y.-1 = - x + x * y
- - y.-1 + - x = - x.+1 + y
    rewrite <- int_neg_add.x: nat
y: Int
IHx: forall y : Int, x * y.-1 = - x + x * y
- (- y.-1 + x) = - x.+1 + y
    rewrite int_neg_pred.x: nat
y: Int
IHx: forall y : Int, x * y.-1 = - x + x * y
- ((- y).+1 + x) = - x.+1 + y
    rewrite int_add_succ_l.x: nat
y: Int
IHx: forall y : Int, x * y.-1 = - x + x * y
- (- y + x).+1 = - x.+1 + y
    rewrite int_add_comm.x: nat
y: Int
IHx: forall y : Int, x * y.-1 = - x + x * y
- (x + - y).+1 = - x.+1 + y
    rewrite <- int_add_succ_l.x: nat
y: Int
IHx: forall y : Int, x * y.-1 = - x + x * y
- (x.+1 + - y) = - x.+1 + y
    rewrite int_neg_add.x: nat
y: Int
IHx: forall y : Int, x * y.-1 = - x + x * y
- x.+1 + - - y = - x.+1 + y
    by rewrite int_neg_neg.
  -x: nat
y: Int
IHx: forall y : Int, - x * y.-1 = - - x + - x * y
(- x).-1 * y.-1 = - (- x).-1 + (- x).-1 * y rewrite int_neg_pred.x: nat
y: Int
IHx: forall y : Int, - x * y.-1 = - - x + - x * y
(- x).-1 * y.-1 = (- - x).+1 + (- x).-1 * y
    rewrite int_neg_neg.x: nat
y: Int
IHx: forall y : Int, - x * y.-1 = - - x + - x * y
(- x).-1 * y.-1 = x.+1 + (- x).-1 * y
    rewrite 2 int_mul_pred_l.x: nat
y: Int
IHx: forall y : Int, - x * y.-1 = - - x + - x * y
- y.-1 + - x * y.-1 = x.+1 + (- y + - x * y)
    rewrite IHx.x: nat
y: Int
IHx: forall y : Int, - x * y.-1 = - - x + - x * y
- y.-1 + (- - x + - x * y) = x.+1 + (- y + - x * y)
    rewrite !int_add_assoc; f_ap.x: nat
y: Int
IHx: forall y : Int, - x * y.-1 = - - x + - x * y
- y.-1 + - - x = x.+1 + - y
    rewrite int_neg_pred.x: nat
y: Int
IHx: forall y : Int, - x * y.-1 = - - x + - x * y
(- y).+1 + - - x = x.+1 + - y
    rewrite int_neg_neg.x: nat
y: Int
IHx: forall y : Int, - x * y.-1 = - - x + - x * y
(- y).+1 + x = x.+1 + - y
    rewrite 2 int_add_succ_l; f_ap.x: nat
y: Int
IHx: forall y : Int, - x * y.-1 = - - x + - x * y
- 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 x : Int, x * y = y * x
x * y.+1 = y.+1 * x
x: Int
y: nat
IHy: forall x : Int, x * - y = - y * x
x * (- y).-1 = (- y).-1 * x
  -x: Int
x * 0 = 0 * x apply int_mul_0_r.
  -x: Int
y: nat
IHy: forall x : Int, x * y = y * x
x * y.+1 = y.+1 * x rewrite int_mul_succ_l.x: Int
y: nat
IHy: forall x : Int, x * y = y * x
x * y.+1 = x + y * x
    rewrite int_mul_succ_r.x: Int
y: nat
IHy: forall x : Int, x * y = y * x
x + x * y = x + y * x
    by rewrite IHy.
  -x: Int
y: nat
IHy: forall x : Int, x * - y = - y * x
x * (- y).-1 = (- y).-1 * x rewrite int_mul_pred_l.x: Int
y: nat
IHy: forall x : Int, x * - y = - y * x
x * (- y).-1 = - x + - y * x
    rewrite int_mul_pred_r.x: Int
y: nat
IHy: forall x : Int, x * - y = - y * x
- 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 y z : Int, x * (y + z) = x * y + x * z
x.+1 * (y + z) = x.+1 * y + x.+1 * z
x: nat
y, z: Int
IHx: forall y z : Int, - x * (y + z) = - x * y + - x * z
(- 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 y z : Int, x * (y + z) = x * y + x * z
x.+1 * (y + z) = x.+1 * y + x.+1 * z rewrite 3 int_mul_succ_l.x: nat
y, z: Int
IHx: forall y z : Int, x * (y + z) = x * y + x * z
y + z + x * (y + z) = y + x * y + (z + x * z)
    rewrite IHx.x: nat
y, z: Int
IHx: forall y z : Int, x * (y + z) = x * y + x * z
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 y z : Int, x * (y + z) = x * y + x * z
y + z + x * y = y + x * y + z
    rewrite <- !int_add_assoc; f_ap.x: nat
y, z: Int
IHx: forall y z : Int, x * (y + z) = x * y + x * z
z + x * y = x * y + z
    by rewrite int_add_comm.
  -x: nat
y, z: Int
IHx: forall y z : Int, - x * (y + z) = - x * y + - x * z
(- x).-1 * (y + z) = (- x).-1 * y + (- x).-1 * z rewrite 3 int_mul_pred_l.x: nat
y, z: Int
IHx: forall y z : Int, - x * (y + z) = - x * y + - x * z
- (y + z) + - x * (y + z) =
- y + - x * y + (- z + - x * z)
    rewrite IHx.x: nat
y, z: Int
IHx: forall y z : Int, - x * (y + z) = - x * y + - x * z
- (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 y z : Int, - x * (y + z) = - x * y + - x * z
- (y + z) + - x * y = - y + - x * y + - z
    rewrite int_neg_add.x: nat
y, z: Int
IHx: forall y z : Int, - x * (y + z) = - x * y + - x * z
- y + - z + - x * y = - y + - x * y + - z
    rewrite <- !int_add_assoc; f_ap.x: nat
y, z: Int
IHx: forall y z : Int, - x * (y + z) = - x * y + - x * z
- 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 y z : Int, x * (y * z) = x * y * z
x.+1 * (y * z) = x.+1 * y * z
x: nat
y, z: Int
IHx: forall y z : Int, - x * (y * z) = - x * y * z
(- 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 y z : Int, x * (y * z) = x * y * z
x.+1 * (y * z) = x.+1 * y * z rewrite 2 int_mul_succ_l.x: nat
y, z: Int
IHx: forall y z : Int, x * (y * z) = x * y * z
y * z + x * (y * z) = (y + x * y) * z
    rewrite int_dist_r.x: nat
y, z: Int
IHx: forall y z : Int, x * (y * z) = x * y * z
y * z + x * (y * z) = y * z + x * y * z
    by rewrite IHx.
  -x: nat
y, z: Int
IHx: forall y z : Int, - x * (y * z) = - x * y * z
(- x).-1 * (y * z) = (- x).-1 * y * z rewrite 2 int_mul_pred_l.x: nat
y, z: Int
IHx: forall y z : Int, - x * (y * z) = - x * y * z
- (y * z) + - x * (y * z) = (- y + - x * y) * z
    rewrite int_dist_r.x: nat
y, z: Int
IHx: forall y z : Int, - x * (y * z) = - x * y * z
- (y * z) + - x * (y * z) = - y * z + - x * y * z
    rewrite <- int_mul_neg_l.x: nat
y, z: Int
IHx: forall y z : Int, - x * (y * z) = - x * y * z
- 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 a : A,
g (int_iter f n a) = int_iter f' n (g a)
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 a : A,
g (int_iter f (- n) a) = int_iter f' (- n) (g a)
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 a : A,
g (int_iter f n a) = int_iter f' n (g a)
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 a : A,
g (int_iter f n a) = int_iter f' n (g a)
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 a : A,
g (int_iter f n a) = int_iter f' n (g a)
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 a : A,
g (int_iter f (- n) a) = int_iter f' (- n) (g a)
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 a : A,
g (int_iter f (- n) a) = int_iter f' (- n) (g a)
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 a : A,
g (int_iter f (- n) a) = int_iter f' (- n) (g a)
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 a : A,
g (int_iter f (- n) a) = int_iter f' (- n) (g a)
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 a : A,
g (int_iter f (- n) a) = int_iter f' (- n) (g a)
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 a : A,
g (int_iter f (- n) a) = int_iter f' (- n) (g a)
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 a : A,
g (int_iter f (- n) a) = int_iter f' (- n) (g a)
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 x : A, P x -> P (f x)
Ppred: forall x : A, P x -> P (f^-1 x)
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 x : A, P x -> P (f x)
Ppred: forall x : A, P x -> P (f^-1 x)
IHn: forall x : A, P x -> P (int_iter f n x)
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 x : A, P x -> P (f x)
Ppred: forall x : A, P x -> P (f^-1 x)
IHn: forall x : A, P x -> P (int_iter f (- n) x)
x: A
P x -> P (int_iter f (- n).-1 x)
  -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)
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 x : A, P x -> P (f x)
Ppred: forall x : A, P x -> P (f^-1 x)
IHn: forall x : A, P x -> P (int_iter f n x)
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 x : A, P x -> P (f x)
Ppred: forall x : A, P x -> P (f^-1 x)
IHn: forall x : A, P x -> P (int_iter f n x)
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 x : A, P x -> P (f x)
Ppred: forall x : A, P x -> P (f^-1 x)
IHn: forall x : A, P x -> P (int_iter f n x)
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 x : A, P x -> P (f x)
Ppred: forall x : A, P x -> P (f^-1 x)
IHn: forall x : A, P x -> P (int_iter f (- n) x)
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 x : A, P x -> P (f x)
Ppred: forall x : A, P x -> P (f^-1 x)
IHn: forall x : A, P x -> P (int_iter f (- n) x)
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 x : A, P x -> P (f x)
Ppred: forall x : A, P x -> P (f^-1 x)
IHn: forall x : A, P x -> P (int_iter f (- n) x)
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.