Core.v

Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids
  Basics.Decidable Basics.Trunc Basics.Equivalences Basics.Nat
  Basics.Classes Basics.Iff Types.Prod Types.Sum Types.Sigma.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Export Basics.Nat.

Local Set Universe Minimization ToSet.
Local Unset Elimination Schemes.

(** * Natural numbers *)

(** We want to close the [trunc_scope] so that notations from there don't conflict here. *)
Local Close Scope trunc_scope.
Local Open Scope nat_scope.

(** ** Basic operations on naturals *)

(** *** Iteration *)

(** [n]th iteration of the function [f : A -> A].  We have definitional equalities [nat_iter 0 f x = x] and [nat_iter n.+1 f x = f (nat_iter n f x)].  We make this a notation, so it doesn't add a universe variable for the universe containing [A]. *)
Notation nat_iter n f x
  := ((fix F (m : nat)
      := match m with
        | 0 => x
        | m'.+1 => f (F m')
        end) n).

(** *** Successor and predecessor *)

(** [nat_succ n] is the successor of a natural number [n]. We defined a notation [x.+1] for it in Overture.v. *)
Notation nat_succ := S (only parsing).

(** [nat_pred n] is the predecessor of a natural number [n]. When [n] is [0] we return [0]. *)
Definition nat_pred n : nat :=
  match n with
  | 0 => n
  | S n' => n'
  end.

(** *** Arithmetic operations *)

(** Addition of natural numbers *)
Definition nat_add n m : nat
  := nat_iter n nat_succ m.

Notation "n + m" := (nat_add n m) : nat_scope.

(** Multiplication of natural numbers *)
Definition nat_mul n m : nat
  := nat_iter n (nat_add m) 0.

Notation "n * m" := (nat_mul n m) : nat_scope.

(** Truncated subtraction: [n - m] is [0] if [n <= m] *)
Fixpoint nat_sub n m : nat :=
  match n, m with
  | S n' , S m' => nat_sub n' m'
  | _ , _ => n
  end.

Notation "n - m" := (nat_sub n m) : nat_scope.

(** Powers or exponentiation of natural numbers. *)
Definition nat_pow n m := nat_iter m (nat_mul n) 1.

(** *** Maximum and minimum *)

(** The maximum [nat_max n m] of two natural numbers [n] and [m]. *)
Fixpoint nat_max n m :=
  match n, m with
  | 0 , _ => m
  | S n' , 0 => n'.+1
  | S n' , S m' => (nat_max n' m').+1
  end.

(** The minimum [nat_min n m] of two natural numbers [n] and [m]. *)
Fixpoint nat_min n m :=
  match n, m with
  | 0 , _ => 0
  | S n' , 0 => 0
  | S n' , S m' => S (nat_min n' m')
  end.

(** *** Euclidean division *)

(** This division takes time linear in `x` and is tail-recursive. In [nat_div_mod x y q u], [x + y.+1 * q + (y - u)] is the quantity being divided and [y] is the predecessor of the divisor.  It will be called with [q] zero and [u] equal to [y], so that [x] is the quantity being divided.  The return value is a pair [(q', u')] with [x + y.+1 * q + (y - u) = y.+1 * q' + (y - u')], at least when [u <= y], as shown in [nat_div_mod_spec_helper] in Nat/Divison.v. *)

Fixpoint nat_div_mod x y q u : nat * nat :=
  match x with
  | 0 => (q , u)
  | S x' =>
    match u with
    | 0 => nat_div_mod x' y (S q) y
    | S u' => nat_div_mod x' y q u'
    end
  end.

Definition nat_div x y : nat :=
  match y with
  | 0 => y
  | S y' => fst (nat_div_mod x y' 0 y')
  end.
Infix "/" := nat_div : nat_scope.

(** [nat_mod x y] is the remainder when [x] is divided by [y].  When [y] is zero, it is defined to be [x]. See [nat_div_mod_spec] and related results below. *)
Definition nat_mod x y : nat :=
  match y with
  | 0 => x
  | S y' => y' - snd (nat_div_mod x y' 0 y')
  end.
Infix "mod" := nat_mod : nat_scope.

(** For results about division and modulo, see Nat/Division.v. *)

(** *** Greatest common divisor *)

(** We use Euclid algorithm, which is normally not structural, but Coq is now clever enough to accept this (behind modulo there is a subtraction, which now preserves being a subterm) *)

Fixpoint nat_gcd a b :=
  match a with
  | O => b
  | S a' => nat_gcd (b mod a'.+1) a'.+1
  end.

(** ** Comparison predicates *)

(** *** Less than or equal To [<=] *)

Inductive leq (n : nat) : nat -> Type0 :=
| leq_refl : leq n n
| leq_succ_r m : leq n m -> leq n (S m).

Arguments leq_succ_r {n m} _.

Scheme leq_ind := Induction for leq Sort Type.
Scheme leq_rect := Induction for leq Sort Type.
Scheme leq_rec := Induction for leq Sort Type.

Notation "n <= m" := (leq n m) : nat_scope.

Existing Class leq.
Existing Instances leq_refl leq_succ_r.

(** *** Less than [<] *)

(** We define the less-than relation [lt] in terms of [leq] *)
Definition lt n m : Type0 := leq (S n) m.

(** We declare it as an existing class so typeclass search is performed on its goals. *)
Existing Class lt.
#[export] Hint Unfold lt : typeclass_instances.
Infix "<" := lt : nat_scope.

(** *** Greater than or equal To [>=] *)

Definition geq n m := leq m n.
Existing Class geq.
#[export] Hint Unfold geq : typeclass_instances.
Infix ">=" := geq : nat_scope.

(*** Greater Than [>] *)

Definition gt n m := lt m n.
Existing Class gt.
#[export] Hint Unfold gt : typeclass_instances.
Infix ">" := gt : nat_scope.

(** *** Combined comparison predicates *)

Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
Notation "x <= y < z"  := (x <= y /\ y <  z) : nat_scope.
Notation "x < y < z"   := (x <  y /\ y <  z) : nat_scope.
Notation "x < y <= z"  := (x <  y /\ y <= z) : nat_scope.

(** ** Properties of [nat_iter]. *)

Definition nat_iter_succ_r n {A} (f : A -> A) (x : A)
  : nat_iter (S n) f x = nat_iter n f (f x).n: nat
A: Type
f: A -> A
x: A
nat_iter n.+1 f x = nat_iter n f (f x)
Proof.n: nat
A: Type
f: A -> A
x: A
nat_iter n.+1 f x = nat_iter n f (f x)
  simple_induction n n IHn; simpl; trivial.A: Type
f: A -> A
x: A
n: nat
IHn: f (nat_iter n f x) = nat_iter n f (f x)
f (f (nat_iter n f x)) = f (nat_iter n f (f x))
  exact (ap f IHn).
Defined.

Definition nat_iter_add (n m : nat) {A} (f : A -> A) (x : A)
  : nat_iter (n + m) f x = nat_iter n f (nat_iter m f x).n, m: nat
A: Type
f: A -> A
x: A
nat_iter (n + m) f x = nat_iter n f (nat_iter m f x)
Proof.n, m: nat
A: Type
f: A -> A
x: A
nat_iter (n + m) f x = nat_iter n f (nat_iter m f x)
  simple_induction n n IHn; simpl; trivial.m: nat
A: Type
f: A -> A
x: A
n: nat
IHn: nat_iter (n + m) f x = nat_iter n f (nat_iter m f x)
f (nat_iter (n + m) f x) =
f (nat_iter n f (nat_iter m f x))
  exact (ap f IHn).
Defined.

(** Preservation of invariants : if [f : A -> A] preserves the invariant [P], then the iterates of [f] also preserve it. *)
Definition nat_iter_invariant (n : nat) {A} (f : A -> A) (P : A -> Type)
  : (forall x, P x -> P (f x)) -> forall x, P x -> P (nat_iter n f x).n: nat
A: Type
f: A -> A
P: A -> Type
(forall x : A, P x -> P (f x)) ->
forall x : A, P x -> P (nat_iter n f x)
Proof.n: nat
A: Type
f: A -> A
P: A -> Type
(forall x : A, P x -> P (f x)) ->
forall x : A, P x -> P (nat_iter n f x)
  simple_induction n n IHn; simpl; trivial.A: Type
f: A -> A
P: A -> Type
n: nat
IHn: (forall x : A, P x -> P (f x)) -> forall x : A, P x -> P (nat_iter n f x)
(forall x : A, P x -> P (f x)) ->
forall x : A, P x -> P (f (nat_iter n f x))
  intros Hf x Hx.A: Type
f: A -> A
P: A -> Type
n: nat
IHn: (forall x : A, P x -> P (f x)) -> forall x : A, P x -> P (nat_iter n f x)
Hf: forall x : A, P x -> P (f x)
x: A
Hx: P x
P (f (nat_iter n f x))
  apply Hf, IHn; trivial.
Defined.

(** ** Properties of successors *)

(** The predecessor of a successor is the original number. *)
Definition nat_pred_succ@{} n : nat_pred (nat_succ n) = n
  := idpath.

(** The successor of a predecessor is the original as long as there is a strict lower bound. *)
Definition nat_succ_pred'@{} n i : i < n -> nat_succ (nat_pred n) = n.n, i: nat
i < n -> (nat_pred n).+1 = n
Proof.n, i: nat
i < n -> (nat_pred n).+1 = n
  by intros [].
Defined.

(** The most common lower bound is to take [0]. *)
Definition nat_succ_pred@{} n : 0 < n -> nat_succ (nat_pred n) = n
  := nat_succ_pred' n 0.

(** Injectivity of successor. *)
Definition path_nat_succ@{} n m (H : S n = S m) : n = m := ap nat_pred H.
Instance isinj_succ : IsInjective nat_succ := path_nat_succ.

(** Inequality of successors is implied with inequality of the arguments. *)
Definition neq_nat_succ@{} n m : n <> m -> S n <> S m.n, m: nat
n <> m -> n.+1 <> m.+1
Proof.n, m: nat
n <> m -> n.+1 <> m.+1
  intros np q.n, m: nat
np: n <> m
q: n.+1 = m.+1
Empty
  apply np.n, m: nat
np: n <> m
q: n.+1 = m.+1
n = m
  exact (path_nat_succ _ _ q).
Defined.

(** Zero is not the successor of a number. *)
Definition neq_nat_zero_succ@{} n : 0 <> S n.n: nat
0 <> n.+1
Proof.n: nat
0 <> n.+1
  discriminate.
Defined.

(** A natural number cannot be equal to its own successor. *)
Definition neq_nat_succ'@{} n : n <> S n.n: nat
n <> n.+1
Proof.n: nat
n <> n.+1
  simple_induction' n.0 <> 1
n: nat
IH: n <> n.+1
n.+1 <> n.+2
  -0 <> 1 apply neq_nat_zero_succ.
  -n: nat
IH: n <> n.+1
n.+1 <> n.+2 by apply neq_nat_succ.
Defined.

(** ** Truncatedness of natural numbers *)

(** [nat] has decidable paths. *)
Instance decidable_paths_nat@{} : DecidablePaths nat.DecidablePaths nat
Proof.DecidablePaths nat
  intros n m.n, m: nat
Decidable (n = m)
  induction n as [|n IHn] in m |- *; destruct m.Decidable (0 = 0)
m: nat
Decidable (0 = m.+1)
n: nat
IHn: forall m : nat, Decidable (n = m)
Decidable (n.+1 = 0)
n, m: nat
IHn: forall m : nat, Decidable (n = m)
Decidable (n.+1 = m.+1)
  -Decidable (0 = 0) exact (inl idpath).
  -m: nat
Decidable (0 = m.+1) exact (inr (neq_nat_zero_succ m)).
  -n: nat
IHn: forall m : nat, Decidable (n = m)
Decidable (n.+1 = 0) exact (inr (fun p => neq_nat_zero_succ n p^)).
  -n, m: nat
IHn: forall m : nat, Decidable (n = m)
Decidable (n.+1 = m.+1) destruct (IHn m) as [p|q].n, m: nat
IHn: forall m : nat, Decidable (n = m)
p: n = m
Decidable (n.+1 = m.+1)
n, m: nat
IHn: forall m : nat, Decidable (n = m)
q: n <> m
Decidable (n.+1 = m.+1)
    +n, m: nat
IHn: forall m : nat, Decidable (n = m)
p: n = m
Decidable (n.+1 = m.+1) exact (inl (ap S p)).
    +n, m: nat
IHn: forall m : nat, Decidable (n = m)
q: n <> m
Decidable (n.+1 = m.+1) exact (inr (fun p => q (path_nat_succ _ _ p))).
Defined.

(** [nat] is therefore a hset. *)
Instance ishset_nat : IsHSet nat := _.

(** ** Properties of addition *)

(** [0] is the left identity of addition. *)
Definition nat_add_zero_l@{} n : 0 + n = n
  := idpath.

(** [0] is the right identity of addition. *)
Definition nat_add_zero_r@{} n : n + 0 = n.n: nat
n + 0 = n
Proof.n: nat
n + 0 = n
  induction n as [|n IHn].0 + 0 = 0
n: nat
IHn: n + 0 = n
n.+1 + 0 = n.+1
  -0 + 0 = 0 reflexivity.
  -n: nat
IHn: n + 0 = n
n.+1 + 0 = n.+1 apply (ap nat_succ).n: nat
IHn: n + 0 = n
nat_iter n S 0 = n
    exact IHn.
Defined.

(** Adding a successor on the left is the same as adding and then taking the successor. *)
Definition nat_add_succ_l@{} n m : n.+1 + m = (n + m).+1
  := idpath.

(** Adding a successor on the right is the same as adding and then taking the successor. *)
Definition nat_add_succ_r@{} n m : n + m.+1 = (n + m).+1.n, m: nat
n + m.+1 = (n + m).+1
Proof.n, m: nat
n + m.+1 = (n + m).+1
  simple_induction' n; simpl.m: nat
m.+1 = m.+1
m, n: nat
IH: n + m.+1 = (n + m).+1
(n + m.+1).+1 = (n + m).+2
  1: reflexivity.m, n: nat
IH: n + m.+1 = (n + m).+1
(n + m.+1).+1 = (n + m).+2
  exact (ap S IH).
Defined.

(** Addition of natural numbers is commutative. *)
Definition nat_add_comm@{} n m : n + m = m + n.n, m: nat
n + m = m + n
Proof.n, m: nat
n + m = m + n
  induction n.m: nat
0 + m = m + 0
n, m: nat
IHn: n + m = m + n
n.+1 + m = m + n.+1
  -m: nat
0 + m = m + 0 exact (nat_add_zero_r m)^.
  -n, m: nat
IHn: n + m = m + n
n.+1 + m = m + n.+1 rhs napply nat_add_succ_r.n, m: nat
IHn: n + m = m + n
n.+1 + m = (m + n).+1
    apply (ap nat_succ).n, m: nat
IHn: n + m = m + n
nat_iter n S m = m + n
    exact IHn.
Defined.

(** Addition of natural numbers is associative. *)
Definition nat_add_assoc@{} n m k : n + (m + k) = (n + m) + k.n, m, k: nat
n + (m + k) = n + m + k
Proof.n, m, k: nat
n + (m + k) = n + m + k
  induction n as [|n IHn].m, k: nat
0 + (m + k) = 0 + m + k
n, m, k: nat
IHn: n + (m + k) = n + m + k
n.+1 + (m + k) = n.+1 + m + k
  -m, k: nat
0 + (m + k) = 0 + m + k reflexivity.
  -n, m, k: nat
IHn: n + (m + k) = n + m + k
n.+1 + (m + k) = n.+1 + m + k napply (ap nat_succ).n, m, k: nat
IHn: n + (m + k) = n + m + k
nat_iter n S (m + k) = nat_iter (nat_iter n S m) S k
    exact IHn.
Defined.

(** Addition on the left is injective. *)
Instance isinj_nat_add_l@{} k : IsInjective (nat_add k).k: nat
IsInjective (nat_add k)
Proof.k: nat
IsInjective (nat_add k)
  simple_induction k k Ik; exact _.
Defined.

(** Addition on the right is injective. *)
Definition isinj_nat_add_r@{} k : IsInjective (fun x => nat_add x k).k: nat
IsInjective (fun x : nat => x + k)
Proof.k: nat
IsInjective (fun x : nat => x + k)
  intros x y H.k, x, y: nat
H: x + k = y + k
x = y
  napply (isinj_nat_add_l k).k, x, y: nat
H: x + k = y + k
k + x = k + y
  lhs napply nat_add_comm.k, x, y: nat
H: x + k = y + k
x + k = k + y
  lhs exact H.k, x, y: nat
H: x + k = y + k
y + k = k + y
  napply nat_add_comm.
Defined.

(** A sum being zero is equivalent to both summands being zero. *)
Definition equiv_nat_add_zero n m : n = 0 /\ m = 0 <~> n + m = 0.n, m: nat
(n = 0) * (m = 0) <~> n + m = 0
Proof.n, m: nat
(n = 0) * (m = 0) <~> n + m = 0
  srapply equiv_iff_hprop.n, m: nat
(n = 0) * (m = 0) -> n + m = 0
n, m: nat
n + m = 0 -> (n = 0) * (m = 0)
  -n, m: nat
(n = 0) * (m = 0) -> n + m = 0 intros [-> ->]; reflexivity.
  -n, m: nat
n + m = 0 -> (n = 0) * (m = 0) destruct n.m: nat
0 + m = 0 -> (0 = 0) * (m = 0)
n, m: nat
n.+1 + m = 0 -> (n.+1 = 0) * (m = 0)
    +m: nat
0 + m = 0 -> (0 = 0) * (m = 0) by split.
    +n, m: nat
n.+1 + m = 0 -> (n.+1 = 0) * (m = 0) intros H; symmetry in H.n, m: nat
H: 0 = n.+1 + m
((n.+1 = 0) * (m = 0))%type
      by apply neq_nat_zero_succ in H.
Defined.

(** ** Properties of multiplication *)

(** Multiplication by [0] on the left is [0]. *)
Definition nat_mul_zero_l@{} n : 0 * n = 0
  := idpath.

(** Multiplication by [0] on the right is [0]. *)
Definition nat_mul_zero_r@{} n : n * 0 = 0.n: nat
n * 0 = 0
Proof.n: nat
n * 0 = 0
  by induction n.
Defined.

Definition nat_mul_succ_l@{} n m : n.+1 * m = m + n * m
  := idpath.

Definition nat_mul_succ_r@{} n m : n * m.+1 = n * m + n.n, m: nat
n * m.+1 = n * m + n
Proof.n, m: nat
n * m.+1 = n * m + n
  induction n as [|n IHn].m: nat
0 * m.+1 = 0 * m + 0
n, m: nat
IHn: n * m.+1 = n * m + n
n.+1 * m.+1 = n.+1 * m + n.+1
  -m: nat
0 * m.+1 = 0 * m + 0 reflexivity.
  -n, m: nat
IHn: n * m.+1 = n * m + n
n.+1 * m.+1 = n.+1 * m + n.+1 rhs napply nat_add_succ_r.n, m: nat
IHn: n * m.+1 = n * m + n
n.+1 * m.+1 = (n.+1 * m + n).+1
    napply (ap nat_succ).n, m: nat
IHn: n * m.+1 = n * m + n
nat_iter m S (nat_iter n (nat_add m.+1) 0) =
n.+1 * m + n
    rhs_V napply nat_add_assoc.n, m: nat
IHn: n * m.+1 = n * m + n
nat_iter m S (nat_iter n (nat_add m.+1) 0) =
m + (nat_iter n (nat_add m) 0 + n)
    napply (ap (nat_add m)).n, m: nat
IHn: n * m.+1 = n * m + n
nat_iter n (nat_add m.+1) 0 =
nat_iter n (nat_add m) 0 + n
    exact IHn.
Defined.

(** Multiplication of natural numbers is commutative. *)
Definition nat_mul_comm@{} n m : n * m = m * n.n, m: nat
n * m = m * n
Proof.n, m: nat
n * m = m * n
  induction m as [|m IHm]; simpl.n: nat
n * 0 = 0
n, m: nat
IHm: n * m = m * n
n * m.+1 = n + m * n
  -n: nat
n * 0 = 0 napply nat_mul_zero_r.
  -n, m: nat
IHm: n * m = m * n
n * m.+1 = n + m * n lhs napply nat_mul_succ_r.n, m: nat
IHm: n * m = m * n
n * m + n = n + m * n
    lhs napply nat_add_comm.n, m: nat
IHm: n * m = m * n
n + n * m = n + m * n
    snapply (ap (nat_add n)).n, m: nat
IHm: n * m = m * n
n * m = m * n
    exact IHm.
Defined.

(** Multiplication of natural numbers distributes over addition on the left. *)
Definition nat_dist_l@{} n m k : n * (m + k) = n * m + n * k.n, m, k: nat
n * (m + k) = n * m + n * k
Proof.n, m, k: nat
n * (m + k) = n * m + n * k
  induction n as [|n IHn]; simpl.m, k: nat
0 = 0
n, m, k: nat
IHn: n * (m + k) = n * m + n * k
m + k + n * (m + k) = m + n * m + (k + n * k)
  -m, k: nat
0 = 0 reflexivity.
  -n, m, k: nat
IHn: n * (m + k) = n * m + n * k
m + k + n * (m + k) = m + n * m + (k + n * k) lhs_V napply nat_add_assoc.n, m, k: nat
IHn: n * (m + k) = n * m + n * k
m + (k + n * (m + k)) = m + n * m + (k + n * k)
    rhs_V napply nat_add_assoc.n, m, k: nat
IHn: n * (m + k) = n * m + n * k
m + (k + n * (m + k)) = m + (n * m + (k + n * k))
    napply (ap (nat_add m)).n, m, k: nat
IHn: n * (m + k) = n * m + n * k
k + n * (m + k) = n * m + (k + n * k)
    lhs napply nat_add_comm.n, m, k: nat
IHn: n * (m + k) = n * m + n * k
n * (m + k) + k = n * m + (k + n * k)
    rewrite IHn.n, m, k: nat
IHn: n * (m + k) = n * m + n * k
n * m + n * k + k = n * m + (k + n * k)
    lhs_V napply nat_add_assoc.n, m, k: nat
IHn: n * (m + k) = n * m + n * k
n * m + (n * k + k) = n * m + (k + n * k)
    napply (ap (nat_add (n * m))).n, m, k: nat
IHn: n * (m + k) = n * m + n * k
n * k + k = k + n * k
    napply nat_add_comm.
Defined.

(** Multiplication of natural numbers distributes over addition on the right. *)
Definition nat_dist_r@{} n m k : (n + m) * k = n * k + m * k.n, m, k: nat
(n + m) * k = n * k + m * k
Proof.n, m, k: nat
(n + m) * k = n * k + m * k
  lhs napply nat_mul_comm.n, m, k: nat
k * (n + m) = n * k + m * k
  lhs napply nat_dist_l.n, m, k: nat
k * n + k * m = n * k + m * k
  napply ap011; napply nat_mul_comm.
Defined.

(** Multiplication of natural numbers is associative. *)
Definition nat_mul_assoc@{} n m k : n * (m * k) = n * m * k.n, m, k: nat
n * (m * k) = n * m * k
Proof.n, m, k: nat
n * (m * k) = n * m * k
  induction n as [|n IHn]; simpl.m, k: nat
0 = 0
n, m, k: nat
IHn: n * (m * k) = n * m * k
m * k + n * (m * k) = (m + n * m) * k
  -m, k: nat
0 = 0 reflexivity.
  -n, m, k: nat
IHn: n * (m * k) = n * m * k
m * k + n * (m * k) = (m + n * m) * k rhs napply nat_dist_r.n, m, k: nat
IHn: n * (m * k) = n * m * k
m * k + n * (m * k) = m * k + n * m * k
    napply (ap (nat_add (m * k))).n, m, k: nat
IHn: n * (m * k) = n * m * k
n * (m * k) = n * m * k
    exact IHn.
Defined.

(** Multiplication by [1] on the left is the identity. *)
Definition nat_mul_one_l@{} n : 1 * n = n
  := nat_add_zero_r _.

(** Multiplication by [1] on the right is the identity. *)
Definition nat_mul_one_r@{} n : n * 1 = n
  := nat_mul_comm _ _ @ nat_mul_one_l _.

(** ** Basic properties of comparison predicates *)

(** *** Basic properties of [<=] *)

(** [<=] is reflexive by definition. *)
Instance reflexive_leq : Reflexive leq := leq_refl.

(** Being less than or equal to is a transitive relation. *)
Definition leq_trans {x y z} : x <= y -> y <= z -> x <= z.x, y, z: nat
x <= y -> y <= z -> x <= z
Proof.x, y, z: nat
x <= y -> y <= z -> x <= z
  intros H1 H2; induction H2; exact _.
Defined.
Hint Immediate leq_trans : typeclass_instances.

(** [<=] is transitive. *)
Instance transitive_leq : Transitive leq := @leq_trans.

(** [0] is less than or equal to any natural number. *)
Definition leq_zero_l n : 0 <= n.n: nat
0 <= n
Proof.n: nat
0 <= n
  simple_induction' n; exact _.
Defined.
Existing Instance leq_zero_l | 10.

Instance pred_leq {m} : nat_pred m <= m.m: nat
nat_pred m <= m
Proof.m: nat
nat_pred m <= m
  destruct m; exact _.
Defined.

(** A predecessor is less than or equal to a predecessor if the original number is less than or equal. *)
Instance leq_pred {n m} : n <= m -> nat_pred n <= nat_pred m.n, m: nat
n <= m -> nat_pred n <= nat_pred m
Proof.n, m: nat
n <= m -> nat_pred n <= nat_pred m
  intros H; induction H; exact _.
Defined.

(** A successor is less than or equal to a successor if the original numbers are less than or equal. *)
Definition leq_succ {n m} : n <= m -> n.+1 <= m.+1.n, m: nat
n <= m -> n.+1 <= m.+1
Proof.n, m: nat
n <= m -> n.+1 <= m.+1
  induction 1; exact _.
Defined.
Existing Instance leq_succ | 100.

(** The converse to [leq_succ] also holds. *)
Definition leq_pred' {n m} : n.+1 <= m.+1 -> n <= m := leq_pred.
Hint Immediate leq_pred' : typeclass_instances.

(** [<] is an irreflexive relation. *)
Definition lt_irrefl n : ~ (n < n).n: nat
~ (n < n)
Proof.n: nat
~ (n < n)
  induction n as [|n IHn].~ (0 < 0)
n: nat
IHn: ~ (n < n)
~ (n.+1 < n.+1)
  1: intro p; inversion p.n: nat
IHn: ~ (n < n)
~ (n.+1 < n.+1)
  intros p; by apply IHn, leq_pred'.
Defined.

Instance irreflexive_lt : Irreflexive lt := lt_irrefl.
Instance irreflexive_gt : Irreflexive gt := lt_irrefl.

(** [<=] is an antisymmetric relation. *)
Definition leq_antisym {x y} : x <= y -> y <= x -> x = y.x, y: nat
x <= y -> y <= x -> x = y
Proof.x, y: nat
x <= y -> y <= x -> x = y
  intros p q.x, y: nat
p: x <= y
q: y <= x
x = y
  destruct p.x: nat
q: x <= x
x = x
x, m: nat
p: x <= m
q: m.+1 <= x
x = m.+1
  1: reflexivity.x, m: nat
p: x <= m
q: m.+1 <= x
x = m.+1
  destruct x; [inversion q|].x, m: nat
p: x.+1 <= m
q: m.+1 <= x.+1
x.+1 = m.+1
  apply leq_pred' in q.x, m: nat
p: x.+1 <= m
q: m <= x
x.+1 = m.+1
  contradiction (lt_irrefl _ (leq_trans p q)).
Defined.

Instance antisymmetric_leq : AntiSymmetric leq := @leq_antisym.
Instance antisymemtric_geq : AntiSymmetric geq
  := fun _ _ p q => leq_antisym q p.

(** Every natural number is zero or greater than zero. *)
Definition nat_zero_or_gt_zero n : (0 = n) + (0 < n).n: nat
((0 = n) + (0 < n))%type
Proof.n: nat
((0 = n) + (0 < n))%type
  induction n as [|n IHn].((0 = 0) + (0 < 0))%type
n: nat
IHn: ((0 = n) + (0 < n))%type
((0 = n.+1) + (0 < n.+1))%type
  1: left; reflexivity.n: nat
IHn: ((0 = n) + (0 < n))%type
((0 = n.+1) + (0 < n.+1))%type
  right; exact _.
Defined.

(** Being less than or equal to [0] implies being [0]. *)
Definition path_zero_leq_zero_r n : n <= 0 -> n = 0.n: nat
n <= 0 -> n = 0
Proof.n: nat
n <= 0 -> n = 0
  intros H; rapply leq_antisym.
Defined.

(** Nothing can be less than [0]. *)
Definition not_lt_zero_r n : ~ (n < 0).n: nat
~ (n < 0)
Proof.n: nat
~ (n < 0)
  intros p.n: nat
p: n < 0
Empty
  apply (lt_irrefl n), (leq_trans p).n: nat
p: n < 0
0 <= n
  exact _.
Defined.

(** [n.+1 <= m] implies [n <= m]. *)
Definition leq_succ_l {n m} : n.+1 <= m -> n <= m.n, m: nat
n.+1 <= m -> n <= m
Proof.n, m: nat
n.+1 <= m -> n <= m
  intro l; apply leq_pred'; exact _.
Defined.

(** A general form for injectivity of this constructor *)
Definition leq_refl_inj_gen n k (p : n <= k) (r : n = k) : p = r # leq_refl n.n, k: nat
p: n <= k
r: n = k
p = transport (leq n) r (leq_refl n)
Proof.n, k: nat
p: n <= k
r: n = k
p = transport (leq n) r (leq_refl n)
  destruct p.n: nat
r: n = n
leq_refl n = transport (leq n) r (leq_refl n)
n, m: nat
p: n <= m
r: n = m.+1
leq_succ_r p = transport (leq n) r (leq_refl n)
  +n: nat
r: n = n
leq_refl n = transport (leq n) r (leq_refl n) assert (c : idpath = r) by apply path_ishprop.n: nat
r: n = n
c: 1 = r
leq_refl n = transport (leq n) r (leq_refl n)
    destruct c.n: nat
leq_refl n = transport (leq n) 1 (leq_refl n)
    reflexivity.
  +n, m: nat
p: n <= m
r: n = m.+1
leq_succ_r p = transport (leq n) r (leq_refl n) destruct r^.m: nat
p: m.+1 <= m
r: m.+1 = m.+1
leq_succ_r p = transport (leq m.+1) r (leq_refl m.+1)
    contradiction (lt_irrefl _ p).
Defined.

(** Which we specialise to this lemma *)
Definition leq_refl_inj n (p : n <= n) : p = leq_refl n
  := leq_refl_inj_gen n n p idpath.

Fixpoint leq_succ_r_inj_gen n m k (p : n <= k) (q : n <= m) (r : m.+1 = k)
  : p = r # leq_succ_r q.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m, k: nat
p: n <= k
q: n <= m
r: m.+1 = k
p = transport (leq n) r (leq_succ_r q)
Proof.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m, k: nat
p: n <= k
q: n <= m
r: m.+1 = k
p = transport (leq n) r (leq_succ_r q)
  revert m q r.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, k: nat
p: n <= k
forall (m : nat) (q : n <= m) 
(r : m.+1 = k), p = transport (leq n) r (leq_succ_r q)
  destruct p.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n: nat
forall (m : nat) (q : n <= m) 
(r : m.+1 = n),
leq_refl n = transport (leq n) r (leq_succ_r q)
leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m: nat
p: n <= m
forall (m0 : nat) 
(q : n <= m0) (r : m0.+1 = m.+1),
leq_succ_r p = transport (leq n) r (leq_succ_r q)
  +leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n: nat
forall (m : nat) (q : n <= m) 
(r : m.+1 = n),
leq_refl n = transport (leq n) r (leq_succ_r q) intros k p r.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, k: nat
p: n <= k
r: k.+1 = n
leq_refl n = transport (leq n) r (leq_succ_r p)
    destruct r.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
k: nat
p: k.+1 <= k
leq_refl k.+1 = transport (leq k.+1) 1 (leq_succ_r p)
    contradiction (lt_irrefl _ p).
  +leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m: nat
p: n <= m
forall (m0 : nat) 
(q : n <= m0) (r : m0.+1 = m.+1),
leq_succ_r p = transport (leq n) r (leq_succ_r q) intros m' q r.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m: nat
p: n <= m
m': nat
q: n <= m'
r: m'.+1 = m.+1
leq_succ_r p = transport (leq n) r (leq_succ_r q)
    pose (r' := path_nat_succ _ _ r).leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m: nat
p: n <= m
m': nat
q: n <= m'
r: m'.+1 = m.+1
r':= path_nat_succ m' m r: m' = m
leq_succ_r p = transport (leq n) r (leq_succ_r q)
    destruct r'.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m': nat
p, q: n <= m'
r: m'.+1 = m'.+1
leq_succ_r p = transport (leq n) r (leq_succ_r q)
    assert (t : idpath = r) by apply path_ishprop.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m': nat
p, q: n <= m'
r: m'.+1 = m'.+1
t: 1 = r
leq_succ_r p = transport (leq n) r (leq_succ_r q)
    destruct t.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m': nat
p, q: n <= m'
leq_succ_r p = transport (leq n) 1 (leq_succ_r q)
    cbn.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m': nat
p, q: n <= m'
leq_succ_r p = leq_succ_r q apply ap.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m': nat
p, q: n <= m'
p = q
    destruct q.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n: nat
p: n <= n
p = leq_refl n
leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m: nat
p: n <= m.+1
q: n <= m
p = leq_succ_r q
    1:  apply leq_refl_inj.leq_succ_r_inj_gen: forall (n m k : nat) 
(p : n <= k) (q : n <= m)
(r : m.+1 = k),
p =
transport (leq n) r
  (leq_succ_r q)
n, m: nat
p: n <= m.+1
q: n <= m
p = leq_succ_r q
    exact (leq_succ_r_inj_gen n m _ p q idpath).
Defined.

Definition leq_succ_r_inj n m (p : n <= m.+1) (q : n <= m) : p = leq_succ_r q
  := leq_succ_r_inj_gen n m m.+1 p q idpath.

Instance ishprop_leq n m : IsHProp (n <= m).n, m: nat
IsHProp (n <= m)
Proof.n, m: nat
IsHProp (n <= m)
  apply hprop_allpath.n, m: nat
forall x y : n <= m, x = y
  intros p q; revert p.n, m: nat
q: n <= m
forall p : n <= m, p = q
  induction q.n: nat
forall p : n <= n, p = leq_refl n
n, m: nat
q: n <= m
IHq: forall p : n <= m, p = q
forall p : n <= m.+1, p = leq_succ_r q
  +n: nat
forall p : n <= n, p = leq_refl n intros y.n: nat
y: n <= n
y = leq_refl n
    rapply leq_refl_inj.
  +n, m: nat
q: n <= m
IHq: forall p : n <= m, p = q
forall p : n <= m.+1, p = leq_succ_r q intros y.n, m: nat
q: n <= m
IHq: forall p : n <= m, p = q
y: n <= m.+1
y = leq_succ_r q
    rapply leq_succ_r_inj.
Defined.

Definition equiv_leq_succ n m : n.+1 <= m.+1 <~> n <= m.n, m: nat
n.+1 <= m.+1 <~> n <= m
Proof.n, m: nat
n.+1 <= m.+1 <~> n <= m
  srapply equiv_iff_hprop.
Defined.

Instance decidable_leq n m : Decidable (n <= m).n, m: nat
Decidable (n <= m)
Proof.n, m: nat
Decidable (n <= m)
  revert n.m: nat
forall n : nat, Decidable (n <= m)
  simple_induction' m; intros n.n: nat
Decidable (n <= 0)
m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
Decidable (n <= m.+1)
  -n: nat
Decidable (n <= 0) destruct n.Decidable (0 <= 0)
n: nat
Decidable (n.+1 <= 0)
    +Decidable (0 <= 0) left; exact _.
    +n: nat
Decidable (n.+1 <= 0) right; apply not_lt_zero_r.
  -m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
Decidable (n <= m.+1) destruct n.m: nat
IH: forall n : nat, Decidable (n <= m)
Decidable (0 <= m.+1)
m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
Decidable (n.+1 <= m.+1)
    +m: nat
IH: forall n : nat, Decidable (n <= m)
Decidable (0 <= m.+1) left; exact _.
    +m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
Decidable (n.+1 <= m.+1) rapply decidable_equiv'.m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
?n <= m <~> n.+1 <= m.+1
      symmetry.m: nat
IH: forall n : nat, Decidable (n <= m)
n: nat
n.+1 <= m.+1 <~> ?n <= m
      apply equiv_leq_succ.
Defined.

(** The default induction principle for [leq] applies to a type family depending on the second variable.  Here is a version involving a type family depending on the first variable. *)
Definition leq_ind_l {n : nat} (Q : forall (m : nat) (l : m <= n.+1), Type)
  (H_Sn : Q n.+1 (leq_refl n.+1))
  (H_m : forall (m : nat) (l : m <= n), Q m (leq_succ_r l))
  : forall (m : nat) (l : m <= n.+1), Q m l.n: nat
Q: forall m : nat, m <= n.+1 -> Type
H_Sn: Q n.+1 (leq_refl n.+1)
H_m: forall (m : nat) (l : m <= n),
Q m (leq_succ_r l)
forall (m : nat) (l : m <= n.+1), Q m l
Proof.n: nat
Q: forall m : nat, m <= n.+1 -> Type
H_Sn: Q n.+1 (leq_refl n.+1)
H_m: forall (m : nat) (l : m <= n),
Q m (leq_succ_r l)
forall (m : nat) (l : m <= n.+1), Q m l
  intros m leq_m_Sn.n: nat
Q: forall m : nat, m <= n.+1 -> Type
H_Sn: Q n.+1 (leq_refl n.+1)
H_m: forall (m : nat) (l : m <= n),
Q m (leq_succ_r l)
m: nat
leq_m_Sn: m <= n.+1
Q m leq_m_Sn
  inversion leq_m_Sn as [p | k H p]; destruct p^; clear p.n: nat
Q: forall m : nat, m <= n.+1 -> Type
H_Sn: Q n.+1 (leq_refl n.+1)
H_m: forall (m : nat) (l : m <= n),
Q m (leq_succ_r l)
leq_m_Sn: n.+1 <= n.+1
Q n.+1 leq_m_Sn
n: nat
Q: forall m : nat, m <= n.+1 -> Type
H_Sn: Q n.+1 (leq_refl n.+1)
H_m: forall (m : nat) (l : m <= n),
Q m (leq_succ_r l)
m: nat
leq_m_Sn: m <= n.+1
H: m <= n
Q m leq_m_Sn
  -n: nat
Q: forall m : nat, m <= n.+1 -> Type
H_Sn: Q n.+1 (leq_refl n.+1)
H_m: forall (m : nat) (l : m <= n),
Q m (leq_succ_r l)
leq_m_Sn: n.+1 <= n.+1
Q n.+1 leq_m_Sn exact (path_ishprop _ _ # H_Sn).
  -n: nat
Q: forall m : nat, m <= n.+1 -> Type
H_Sn: Q n.+1 (leq_refl n.+1)
H_m: forall (m : nat) (l : m <= n),
Q m (leq_succ_r l)
m: nat
leq_m_Sn: m <= n.+1
H: m <= n
Q m leq_m_Sn exact (path_ishprop _ _ # H_m _ _).
Defined.

(** *** Basic properties of [<] *)

(** [<=] and [<] imply [<] *)
Definition lt_leq_lt_trans {n m k} : n <= m -> m < k -> n < k
  := fun leq lt => leq_trans (leq_succ leq) lt.

(** [<=] and [<] imply [<] *)
Definition lt_lt_leq_trans {n m k} : n < m -> m <= k -> n < k
  := fun lt leq => leq_trans lt leq.

Definition leq_lt {n m} : n < m -> n <= m
  := leq_succ_l.
Hint Immediate leq_lt : typeclass_instances.

Definition lt_trans {n m k} : n < m -> m < k -> n < k
  := fun H1 H2 => leq_lt (lt_leq_lt_trans H1 H2).
Hint Immediate lt_trans : typeclass_instances.

Instance transitive_lt : Transitive lt := @lt_trans.
Instance ishprop_lt n m : IsHProp (n < m) := _.
Instance decidable_lt n m : Decidable (lt n m) := _.

(** *** Basic properties of [>=] *)

Instance reflexive_geq : Reflexive geq := leq_refl.
Instance transitive_geq : Transitive geq := fun x y z p q => leq_trans q p.
Instance ishprop_geq n m : IsHProp (geq n m) := _.
Instance decidable_geq n m : Decidable (geq n m) := _.

(** *** Basic properties of [>] *)

Instance transitive_gt : Transitive gt
  := fun x y z p q => transitive_lt _ _ _ q p.
Instance ishprop_gt n m : IsHProp (gt n m) := _.
Instance decidable_gt n m : Decidable (gt n m) := _.

(** ** Properties of subtraction *)

(** Subtracting a number from [0] is [0]. *)
Definition nat_sub_zero_l@{} n : 0 - n = 0 := idpath.

(** Subtracting [0] from a number is the number itself. *)
Definition nat_sub_zero_r@{} (n : nat) : n - 0 = n.n: nat
n - 0 = n
Proof.n: nat
n - 0 = n
  destruct n; reflexivity.
Defined.

(** Subtracting a number from itself is [0]. *)
Definition nat_sub_cancel@{} (n : nat) : n - n = 0.n: nat
n - n = 0
Proof.n: nat
n - n = 0
  simple_induction n n IHn.0 - 0 = 0
n: nat
IHn: n - n = 0
n.+1 - n.+1 = 0
  -0 - 0 = 0 reflexivity.
  -n: nat
IHn: n - n = 0
n.+1 - n.+1 = 0 exact IHn.
Defined.

(** Subtracting an addition is the same as subtracting the two numbers separately. *)
Definition nat_sub_r_add@{} n m k : n - (m + k) = n - m - k.n, m, k: nat
n - (m + k) = n - m - k
Proof.n, m, k: nat
n - (m + k) = n - m - k
  induction n as [|n IHn] in m, k |- *.m, k: nat
0 - (m + k) = 0 - m - k
n, m, k: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
n.+1 - (m + k) = n.+1 - m - k
  -m, k: nat
0 - (m + k) = 0 - m - k reflexivity.
  -n, m, k: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
n.+1 - (m + k) = n.+1 - m - k destruct m.n, k: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
n.+1 - (0 + k) = n.+1 - 0 - k
n, m, k: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
n.+1 - (m.+1 + k) = n.+1 - m.+1 - k
    +n, k: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
n.+1 - (0 + k) = n.+1 - 0 - k reflexivity.
    +n, m, k: nat
IHn: forall m k : nat, n - (m + k) = n - m - k
n.+1 - (m.+1 + k) = n.+1 - m.+1 - k napply IHn.
Defined.

(** The order in which two numbers are subtracted does not matter. *)
Definition nat_sub_comm_r@{} n m k : n - m - k = n - k - m.n, m, k: nat
n - m - k = n - k - m
Proof.n, m, k: nat
n - m - k = n - k - m
  lhs_V napply nat_sub_r_add.n, m, k: nat
n - (m + k) = n - k - m
  rewrite nat_add_comm.n, m, k: nat
n - (k + m) = n - k - m
  napply nat_sub_r_add.
Defined.

(** Subtracting a larger number from a smaller number is [0]. *)
Definition equiv_nat_sub_leq {n m} : n <= m <~> n - m = 0.n, m: nat
n <= m <~> n - m = 0
Proof.n, m: nat
n <= m <~> n - m = 0
  srapply equiv_iff_hprop.n, m: nat
n <= m -> n - m = 0
n, m: nat
n - m = 0 -> n <= m
  -n, m: nat
n <= m -> n - m = 0 intro l; induction l.n: nat
n - n = 0
n, m: nat
l: n <= m
IHl: n - m = 0
n - m.+1 = 0
    +n: nat
n - n = 0 exact (nat_sub_cancel n).
    +n, m: nat
l: n <= m
IHl: n - m = 0
n - m.+1 = 0 change (m.+1) with (1 + m).n, m: nat
l: n <= m
IHl: n - m = 0
n - (1 + m) = 0
      lhs napply nat_sub_r_add.n, m: nat
l: n <= m
IHl: n - m = 0
n - 1 - m = 0
      lhs napply nat_sub_comm_r.n, m: nat
l: n <= m
IHl: n - m = 0
n - m - 1 = 0
      by destruct IHl^.
  -n, m: nat
n - m = 0 -> n <= m induction n as [|n IHn] in m |- *.m: nat
0 - m = 0 -> 0 <= m
n, m: nat
IHn: forall m : nat, n - m = 0 -> n <= m
n.+1 - m = 0 -> n.+1 <= m
    1: intro; exact _.n, m: nat
IHn: forall m : nat, n - m = 0 -> n <= m
n.+1 - m = 0 -> n.+1 <= m
    destruct m.n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
n.+1 - 0 = 0 -> n.+1 <= 0
n, m: nat
IHn: forall m : nat, n - m = 0 -> n <= m
n.+1 - m.+1 = 0 -> n.+1 <= m.+1
    +n: nat
IHn: forall m : nat, n - m = 0 -> n <= m
n.+1 - 0 = 0 -> n.+1 <= 0 intros p; by destruct p.
    +n, m: nat
IHn: forall m : nat, n - m = 0 -> n <= m
n.+1 - m.+1 = 0 -> n.+1 <= m.+1 intros p.n, m: nat
IHn: forall m : nat, n - m = 0 -> n <= m
p: n.+1 - m.+1 = 0
n.+1 <= m.+1
      apply leq_succ, IHn.n, m: nat
IHn: forall m : nat, n - m = 0 -> n <= m
p: n.+1 - m.+1 = 0
n - m = 0
      exact p.
Defined.

(** We can cancel a left summand when subtracting it from a sum. *)
Definition nat_add_sub_cancel_l m n : n + m - n = m.m, n: nat
n + m - n = m
Proof.m, n: nat
n + m - n = m
  induction n as [|n IHn].m: nat
0 + m - 0 = m
m, n: nat
IHn: n + m - n = m
n.+1 + m - n.+1 = m
  -m: nat
0 + m - 0 = m napply nat_sub_zero_r.
  -m, n: nat
IHn: n + m - n = m
n.+1 + m - n.+1 = m exact IHn.
Defined.

(** We can cancel a right summand when subtracting it from a sum. *)
Definition nat_add_sub_cancel_r m n : m + n - n = m.m, n: nat
m + n - n = m
Proof.m, n: nat
m + n - n = m
  rhs_V exact (nat_add_sub_cancel_l m n).m, n: nat
m + n - n = n + m - n
  napply (ap (fun x => x - n)).m, n: nat
m + n = n + m
  napply nat_add_comm.
Defined.

(** We can cancel a right subtrahend when adding it on the right to a subtraction if the subtrahend is less than the number being subtracted from. *)
Definition nat_add_sub_l_cancel {n m} : n <= m -> (m - n) + n = m.n, m: nat
n <= m -> m - n + n = m
Proof.n, m: nat
n <= m -> m - n + n = m
  intros H.n, m: nat
H: n <= m
m - n + n = m
  induction n as [|n IHn] in m, H |- *.m: nat
H: 0 <= m
m - 0 + 0 = m
n, m: nat
H: n.+1 <= m
IHn: forall m : nat, n <= m -> m - n + n = m
m - n.+1 + n.+1 = m
  -m: nat
H: 0 <= m
m - 0 + 0 = m lhs napply nat_add_zero_r.m: nat
H: 0 <= m
m - 0 = m
    napply nat_sub_zero_r.
  -n, m: nat
H: n.+1 <= m
IHn: forall m : nat, n <= m -> m - n + n = m
m - n.+1 + n.+1 = m destruct m.n: nat
H: n.+1 <= 0
IHn: forall m : nat, n <= m -> m - n + n = m
0 - n.+1 + n.+1 = 0
n, m: nat
H: n.+1 <= m.+1
IHn: forall m : nat, n <= m -> m - n + n = m
m.+1 - n.+1 + n.+1 = m.+1
    1: contradiction (not_lt_zero_r n).n, m: nat
H: n.+1 <= m.+1
IHn: forall m : nat, n <= m -> m - n + n = m
m.+1 - n.+1 + n.+1 = m.+1
    lhs napply nat_add_succ_r.n, m: nat
H: n.+1 <= m.+1
IHn: forall m : nat, n <= m -> m - n + n = m
(m.+1 - n.+1 + n).+1 = m.+1
    napply (ap nat_succ).n, m: nat
H: n.+1 <= m.+1
IHn: forall m : nat, n <= m -> m - n + n = m
m.+1 - n.+1 + n = m
    napply IHn.n, m: nat
H: n.+1 <= m.+1
IHn: forall m : nat, n <= m -> m - n + n = m
n <= m
    exact (leq_pred' H).
Defined.

(** We can cancel a right subtrahend when adding it on the left to a subtraction if the subtrahend is less than the number being subtracted from. *)
Definition nat_add_sub_r_cancel {n m} : n <= m -> n + (m - n) = m.n, m: nat
n <= m -> n + (m - n) = m
Proof.n, m: nat
n <= m -> n + (m - n) = m
  intros H.n, m: nat
H: n <= m
n + (m - n) = m
  rhs_V exact (nat_add_sub_l_cancel H).n, m: nat
H: n <= m
n + (m - n) = m - n + n
  apply nat_add_comm.
Defined.

(** We can move a subtracted number to the left-hand side of an equation. *)
Definition nat_moveL_nV {n m} k : n + k = m -> n = m - k.n, m, k: nat
n + k = m -> n = m - k
Proof.n, m, k: nat
n + k = m -> n = m - k
  intros p.n, m, k: nat
p: n + k = m
n = m - k
  destruct p.n, k: nat
n = n + k - k
  symmetry.n, k: nat
n + k - k = n
  apply nat_add_sub_cancel_r.
Defined.

(** We can move a subtracted number to the right-hand side of an equation. *)
Definition nat_moveR_nV {n m} k : n = m + k -> n - k = m
  := fun p => (nat_moveL_nV _ p^)^.

(** Subtracting a successor is the predecessor of subtracting the original number. *)
Definition nat_sub_succ_r n m : n - m.+1 = nat_pred (n - m).n, m: nat
n - m.+1 = nat_pred (n - m)
Proof.n, m: nat
n - m.+1 = nat_pred (n - m)
  induction n as [|n IHn] in m |- *.m: nat
0 - m.+1 = nat_pred (0 - m)
n, m: nat
IHn: forall m : nat, n - m.+1 = nat_pred (n - m)
n.+1 - m.+1 = nat_pred (n.+1 - m)
  1: reflexivity.n, m: nat
IHn: forall m : nat, n - m.+1 = nat_pred (n - m)
n.+1 - m.+1 = nat_pred (n.+1 - m)
  destruct m.n: nat
IHn: forall m : nat, n - m.+1 = nat_pred (n - m)
n.+1 - 1 = nat_pred (n.+1 - 0)
n, m: nat
IHn: forall m : nat, n - m.+1 = nat_pred (n - m)
n.+1 - m.+2 = nat_pred (n.+1 - m.+1)
  1: apply nat_sub_zero_r.n, m: nat
IHn: forall m : nat, n - m.+1 = nat_pred (n - m)
n.+1 - m.+2 = nat_pred (n.+1 - m.+1)
  apply IHn.
Defined.

(** ** Properties of maximum and minimum *)

(** *** Properties of maximum *)

(** [nat_max] is idempotent. *)
Definition nat_max_idem@{} n : nat_max n n = n.n: nat
nat_max n n = n
Proof.n: nat
nat_max n n = n
  simple_induction' n; cbn.0 = 0
n: nat
IH: nat_max n n = n
(nat_max n n).+1 = n.+1
  1: reflexivity.n: nat
IH: nat_max n n = n
(nat_max n n).+1 = n.+1
  exact (ap S IH).
Defined.

(** The defining properties of [nat_max]: [m] and [n] are less than or equal to [nat_max n m] and [nat_max n m] is less than or equal to any number greater than or equal to [m] and [n]. *)
Definition leq_nat_max_l@{} n m : n <= nat_max n m.n, m: nat
n <= nat_max n m
Proof.n, m: nat
n <= nat_max n m
  induction n as [|n IHn] in m |- *.m: nat
0 <= nat_max 0 m
n, m: nat
IHn: forall m : nat, n <= nat_max n m
n.+1 <= nat_max n.+1 m
  1: exact (leq_zero_l _).n, m: nat
IHn: forall m : nat, n <= nat_max n m
n.+1 <= nat_max n.+1 m
  destruct m; cbn.n: nat
IHn: forall m : nat, n <= nat_max n m
n.+1 <= n.+1
n, m: nat
IHn: forall m : nat, n <= nat_max n m
n.+1 <= (nat_max n m).+1
  1: cbn; reflexivity.n, m: nat
IHn: forall m : nat, n <= nat_max n m
n.+1 <= (nat_max n m).+1
  exact (leq_succ (IHn m)).
Defined.

Definition leq_nat_max_r@{} n m : m <= nat_max n m.n, m: nat
m <= nat_max n m
Proof.n, m: nat
m <= nat_max n m
  induction n as [|n IHn] in m |- *.m: nat
m <= nat_max 0 m
n, m: nat
IHn: forall m : nat, m <= nat_max n m
m <= nat_max n.+1 m
  1: cbn; reflexivity.n, m: nat
IHn: forall m : nat, m <= nat_max n m
m <= nat_max n.+1 m
  destruct m; cbn.n: nat
IHn: forall m : nat, m <= nat_max n m
0 <= n.+1
n, m: nat
IHn: forall m : nat, m <= nat_max n m
m.+1 <= (nat_max n m).+1
  1: exact (leq_zero_l _).n, m: nat
IHn: forall m : nat, m <= nat_max n m
m.+1 <= (nat_max n m).+1
  exact (leq_succ (IHn m)).
Defined.

Definition leq_nat_max@{} {n m k : nat} (Hn : n <= k) (Hm : m <= k)
  : nat_max n m <= k.n, m, k: nat
Hn: n <= k
Hm: m <= k
nat_max n m <= k
Proof.n, m, k: nat
Hn: n <= k
Hm: m <= k
nat_max n m <= k
  induction k in m, n, Hn, Hm |- *; destruct m, n; cbn.Hn, Hm: 0 <= 0
0 <= 0
n: nat
Hn: n.+1 <= 0
Hm: 0 <= 0
n.+1 <= 0
m: nat
Hn: 0 <= 0
Hm: m.+1 <= 0
m.+1 <= 0
n, m: nat
Hn: n.+1 <= 0
Hm: m.+1 <= 0
(nat_max n m).+1 <= 0
k: nat
Hn, Hm: 0 <= k.+1
IHk: forall n m : nat, n <= k -> m <= k -> nat_max n m <= k
0 <= k.+1
n, k: nat
Hn: n.+1 <= k.+1
Hm: 0 <= k.+1
IHk: forall n m : nat, n <= k -> m <= k -> nat_max n m <= k
n.+1 <= k.+1
m, k: nat
Hn: 0 <= k.+1
Hm: m.+1 <= k.+1
IHk: forall n m : nat, n <= k -> m <= k -> nat_max n m <= k
m.+1 <= k.+1
n, m, k: nat
Hn: n.+1 <= k.+1
Hm: m.+1 <= k.+1
IHk: forall n m : nat, n <= k -> m <= k -> nat_max n m <= k
(nat_max n m).+1 <= k.+1
  1-3, 5-7: exact _.n, m: nat
Hn: n.+1 <= 0
Hm: m.+1 <= 0
(nat_max n m).+1 <= 0
n, m, k: nat
Hn: n.+1 <= k.+1
Hm: m.+1 <= k.+1
IHk: forall n m : nat, n <= k -> m <= k -> nat_max n m <= k
(nat_max n m).+1 <= k.+1
  -n, m: nat
Hn: n.+1 <= 0
Hm: m.+1 <= 0
(nat_max n m).+1 <= 0 contradiction (not_lt_zero_r _ _).
  -n, m, k: nat
Hn: n.+1 <= k.+1
Hm: m.+1 <= k.+1
IHk: forall n m : nat, n <= k -> m <= k -> nat_max n m <= k
(nat_max n m).+1 <= k.+1 exact (leq_succ (IHk n m _ _)).
Defined.

(** [nat_max] is commutative. *)
Definition nat_max_comm@{} n m : nat_max n m = nat_max m n.n, m: nat
nat_max n m = nat_max m n
Proof.n, m: nat
nat_max n m = nat_max m n
  induction n as [|n IHn] in m |- *; destruct m; cbn.0 = 0
m: nat
m.+1 = m.+1
n: nat
IHn: forall m : nat, nat_max n m = nat_max m n
n.+1 = n.+1
n, m: nat
IHn: forall m : nat, nat_max n m = nat_max m n
(nat_max n m).+1 = (nat_max m n).+1
  1-3: reflexivity.n, m: nat
IHn: forall m : nat, nat_max n m = nat_max m n
(nat_max n m).+1 = (nat_max m n).+1
  exact (ap S (IHn _)).
Defined.

(** The maximum of [n.+1] and [n] is [n.+1]. *)
Definition nat_max_succ_l@{} n : nat_max n.+1 n = n.+1.n: nat
nat_max n.+1 n = n.+1
Proof.n: nat
nat_max n.+1 n = n.+1
  simple_induction' n; cbn.1 = 1
n: nat
IH: nat_max n.+1 n = n.+1
match n with
| 0 => n.+1
| m'.+1 => (nat_max n m').+1
end.+1 = n.+2
  1: reflexivity.n: nat
IH: nat_max n.+1 n = n.+1
match n with
| 0 => n.+1
| m'.+1 => (nat_max n m').+1
end.+1 = n.+2
  exact (ap S IH).
Defined.

(** The maximum of [n] and [n.+1] is [n.+1]. *)
Definition nat_max_succ_r@{} n : nat_max n n.+1 = n.+1
  := nat_max_comm _ _ @ nat_max_succ_l _.

(** [0] is the left identity of [nat_max]. *)
Definition nat_max_zero_l@{} n : nat_max 0 n = n := idpath.

(** [0] is the right identity of [nat_max]. *)
Definition nat_max_zero_r@{} n : nat_max n 0 = n
  := nat_max_comm _ _ @ nat_max_zero_l _.

(** [nat_max n m] is [n] if [m <= n]. *)
Definition nat_max_l@{} {n m} : m <= n -> nat_max n m = n.n, m: nat
m <= n -> nat_max n m = n
Proof.n, m: nat
m <= n -> nat_max n m = n
  intros H.n, m: nat
H: m <= n
nat_max n m = n
  induction m as [|m IHm] in n, H |- *.n: nat
H: 0 <= n
nat_max n 0 = n
n, m: nat
H: m.+1 <= n
IHm: forall n : nat, m <= n -> nat_max n m = n
nat_max n m.+1 = n
  1: napply nat_max_zero_r.n, m: nat
H: m.+1 <= n
IHm: forall n : nat, m <= n -> nat_max n m = n
nat_max n m.+1 = n
  destruct n.m: nat
H: m.+1 <= 0
IHm: forall n : nat, m <= n -> nat_max n m = n
nat_max 0 m.+1 = 0
n, m: nat
H: m.+1 <= n.+1
IHm: forall n : nat, m <= n -> nat_max n m = n
nat_max n.+1 m.+1 = n.+1
  1: inversion H.n, m: nat
H: m.+1 <= n.+1
IHm: forall n : nat, m <= n -> nat_max n m = n
nat_max n.+1 m.+1 = n.+1
  cbn; by apply (ap S), IHm, leq_pred'.
Defined.

(** [nat_max n m] is [m] if [n <= m]. *)
Definition nat_max_r {n m} : n <= m -> nat_max n m = m
  := fun _ => nat_max_comm _ _ @ nat_max_l _.

(** [nat_max n m] is associative. *)
Definition nat_max_assoc@{} n m k
  : nat_max n (nat_max m k) = nat_max (nat_max n m) k.n, m, k: nat
nat_max n (nat_max m k) = nat_max (nat_max n m) k
Proof.n, m, k: nat
nat_max n (nat_max m k) = nat_max (nat_max n m) k
  induction n as [|n IHn] in m, k |- *.m, k: nat
nat_max 0 (nat_max m k) = nat_max (nat_max 0 m) k
n, m, k: nat
IHn: forall m k : nat, nat_max n (nat_max m k) = nat_max (nat_max n m) k
nat_max n.+1 (nat_max m k) =
nat_max (nat_max n.+1 m) k
  1: reflexivity.n, m, k: nat
IHn: forall m k : nat, nat_max n (nat_max m k) = nat_max (nat_max n m) k
nat_max n.+1 (nat_max m k) =
nat_max (nat_max n.+1 m) k
  destruct m, k.n: nat
IHn: forall m k : nat, nat_max n (nat_max m k) = nat_max (nat_max n m) k
nat_max n.+1 (nat_max 0 0) =
nat_max (nat_max n.+1 0) 0
n, k: nat
IHn: forall m k : nat, nat_max n (nat_max m k) = nat_max (nat_max n m) k
nat_max n.+1 (nat_max 0 k.+1) =
nat_max (nat_max n.+1 0) k.+1
n, m: nat
IHn: forall m k : nat, nat_max n (nat_max m k) = nat_max (nat_max n m) k
nat_max n.+1 (nat_max m.+1 0) =
nat_max (nat_max n.+1 m.+1) 0
n, m, k: nat
IHn: forall m k : nat, nat_max n (nat_max m k) = nat_max (nat_max n m) k
nat_max n.+1 (nat_max m.+1 k.+1) =
nat_max (nat_max n.+1 m.+1) k.+1
  1-3: reflexivity.n, m, k: nat
IHn: forall m k : nat, nat_max n (nat_max m k) = nat_max (nat_max n m) k
nat_max n.+1 (nat_max m.+1 k.+1) =
nat_max (nat_max n.+1 m.+1) k.+1
  by apply (ap S), IHn.
Defined.

(** Properties of Minima *)

(** [nat_min] is idempotent. *)
Definition nat_min_idem n : nat_min n n = n.n: nat
nat_min n n = n
Proof.n: nat
nat_min n n = n
  simple_induction' n; cbn.0 = 0
n: nat
IH: nat_min n n = n
(nat_min n n).+1 = n.+1
  1: reflexivity.n: nat
IH: nat_min n n = n
(nat_min n n).+1 = n.+1
  exact (ap S IH).
Defined.

(** The defining properties of [nat_min]: [nat_min n m] is less than or equal to [m] and [n] and any number less than or equal to [m] and [n] is less than or equal to [nat_min n m]. *)
Definition leq_nat_min_l@{} n m : nat_min n m <= n.n, m: nat
nat_min n m <= n
Proof.n, m: nat
nat_min n m <= n
  induction n as [|n IHn] in m |- *.m: nat
nat_min 0 m <= 0
n, m: nat
IHn: forall m : nat, nat_min n m <= n
nat_min n.+1 m <= n.+1
  1: cbn; reflexivity.n, m: nat
IHn: forall m : nat, nat_min n m <= n
nat_min n.+1 m <= n.+1
  destruct m; cbn.n: nat
IHn: forall m : nat, nat_min n m <= n
0 <= n.+1
n, m: nat
IHn: forall m : nat, nat_min n m <= n
(nat_min n m).+1 <= n.+1
  1: exact (leq_zero_l _).n, m: nat
IHn: forall m : nat, nat_min n m <= n
(nat_min n m).+1 <= n.+1
  exact (leq_succ (IHn m)).
Defined.

Definition leq_nat_min_r@{} n m : nat_min n m <= m.n, m: nat
nat_min n m <= m
Proof.n, m: nat
nat_min n m <= m
  induction n as [|n IHn] in m |- *.m: nat
nat_min 0 m <= m
n, m: nat
IHn: forall m : nat, nat_min n m <= m
nat_min n.+1 m <= m
  1: exact (leq_zero_l _).n, m: nat
IHn: forall m : nat, nat_min n m <= m
nat_min n.+1 m <= m
  destruct m; cbn.n: nat
IHn: forall m : nat, nat_min n m <= m
0 <= 0
n, m: nat
IHn: forall m : nat, nat_min n m <= m
(nat_min n m).+1 <= m.+1
  1: cbn; reflexivity.n, m: nat
IHn: forall m : nat, nat_min n m <= m
(nat_min n m).+1 <= m.+1
  exact (leq_succ (IHn m)).
Defined.

Definition leq_nat_min@{} {n m k : nat} (Hn : k <= n) (Hm : k <= m)
  : k <= nat_min n m.n, m, k: nat
Hn: k <= n
Hm: k <= m
k <= nat_min n m
Proof.n, m, k: nat
Hn: k <= n
Hm: k <= m
k <= nat_min n m
  induction k in m, n, Hn, Hm |- *; destruct m, n; cbn.Hn, Hm: 0 <= 0
0 <= 0
n: nat
Hn: 0 <= n.+1
Hm: 0 <= 0
0 <= 0
m: nat
Hn: 0 <= 0
Hm: 0 <= m.+1
0 <= 0
n, m: nat
Hn: 0 <= n.+1
Hm: 0 <= m.+1
0 <= (nat_min n m).+1
k: nat
Hn, Hm: k.+1 <= 0
IHk: forall n m : nat, k <= n -> k <= m -> k <= nat_min n m
k.+1 <= 0
n, k: nat
Hn: k.+1 <= n.+1
Hm: k.+1 <= 0
IHk: forall n m : nat, k <= n -> k <= m -> k <= nat_min n m
k.+1 <= 0
m, k: nat
Hn: k.+1 <= 0
Hm: k.+1 <= m.+1
IHk: forall n m : nat, k <= n -> k <= m -> k <= nat_min n m
k.+1 <= 0
n, m, k: nat
Hn: k.+1 <= n.+1
Hm: k.+1 <= m.+1
IHk: forall n m : nat, k <= n -> k <= m -> k <= nat_min n m
k.+1 <= (nat_min n m).+1
  1-7: exact _.n, m, k: nat
Hn: k.+1 <= n.+1
Hm: k.+1 <= m.+1
IHk: forall n m : nat, k <= n -> k <= m -> k <= nat_min n m
k.+1 <= (nat_min n m).+1
  exact (leq_succ (IHk n m _ _)).
Defined.

(** [nat_min] is commutative. *)
Definition nat_min_comm n m : nat_min n m = nat_min m n.n, m: nat
nat_min n m = nat_min m n
Proof.n, m: nat
nat_min n m = nat_min m n
  induction n as [|n IHn] in m |- *; destruct m; cbn.0 = 0
m: nat
0 = 0
n: nat
IHn: forall m : nat, nat_min n m = nat_min m n
0 = 0
n, m: nat
IHn: forall m : nat, nat_min n m = nat_min m n
(nat_min n m).+1 = (nat_min m n).+1
  1-3: reflexivity.n, m: nat
IHn: forall m : nat, nat_min n m = nat_min m n
(nat_min n m).+1 = (nat_min m n).+1
  exact (ap S (IHn _)).
Defined.

(** [nat_min] of [0] and [n] is [0]. *)
Definition nat_min_zero_l n : nat_min 0 n = 0 := idpath.

(** [nat_min] of [n] and [0] is [0]. *)
Definition nat_min_zero_r n : nat_min n 0 = 0:=
  nat_min_comm _ _ @ nat_min_zero_l _.

(** [nat_min n m] is [n] if [n <= m]. *)
Definition nat_min_l {n m} : n <= m -> nat_min n m = n.n, m: nat
n <= m -> nat_min n m = n
Proof.n, m: nat
n <= m -> nat_min n m = n
  revert n m.forall n m : nat, n <= m -> nat_min n m = n
  simple_induction n n IHn; auto.n: nat
IHn: forall m : nat, n <= m -> nat_min n m = n
forall m : nat, n.+1 <= m -> nat_min n.+1 m = n.+1
  intros [] p.n: nat
IHn: forall m : nat, n <= m -> nat_min n m = n
p: n.+1 <= 0
nat_min n.+1 0 = n.+1
n: nat
IHn: forall m : nat, n <= m -> nat_min n m = n
n0: nat
p: n.+1 <= n0.+1
nat_min n.+1 n0.+1 = n.+1
  1: inversion p.n: nat
IHn: forall m : nat, n <= m -> nat_min n m = n
n0: nat
p: n.+1 <= n0.+1
nat_min n.+1 n0.+1 = n.+1
  cbn; by apply (ap S), IHn, leq_pred'.
Defined.

(** [nat_min n m] is [m] if [m <= n]. *)
Definition nat_min_r {n m} : m <= n -> nat_min n m = m
  := fun _ => nat_min_comm _ _ @ nat_min_l _.

(** [nat_min n m] is associative. *)
Definition nat_min_assoc n m k
  : nat_min n (nat_min m k) = nat_min (nat_min n m) k.n, m, k: nat
nat_min n (nat_min m k) = nat_min (nat_min n m) k
Proof.n, m, k: nat
nat_min n (nat_min m k) = nat_min (nat_min n m) k
  induction n as [|n IHn] in m, k |- *.m, k: nat
nat_min 0 (nat_min m k) = nat_min (nat_min 0 m) k
n, m, k: nat
IHn: forall m k : nat, nat_min n (nat_min m k) = nat_min (nat_min n m) k
nat_min n.+1 (nat_min m k) =
nat_min (nat_min n.+1 m) k
  1: reflexivity.n, m, k: nat
IHn: forall m k : nat, nat_min n (nat_min m k) = nat_min (nat_min n m) k
nat_min n.+1 (nat_min m k) =
nat_min (nat_min n.+1 m) k
  destruct m, k.n: nat
IHn: forall m k : nat, nat_min n (nat_min m k) = nat_min (nat_min n m) k
nat_min n.+1 (nat_min 0 0) =
nat_min (nat_min n.+1 0) 0
n, k: nat
IHn: forall m k : nat, nat_min n (nat_min m k) = nat_min (nat_min n m) k
nat_min n.+1 (nat_min 0 k.+1) =
nat_min (nat_min n.+1 0) k.+1
n, m: nat
IHn: forall m k : nat, nat_min n (nat_min m k) = nat_min (nat_min n m) k
nat_min n.+1 (nat_min m.+1 0) =
nat_min (nat_min n.+1 m.+1) 0
n, m, k: nat
IHn: forall m k : nat, nat_min n (nat_min m k) = nat_min (nat_min n m) k
nat_min n.+1 (nat_min m.+1 k.+1) =
nat_min (nat_min n.+1 m.+1) k.+1
  1-3: reflexivity.n, m, k: nat
IHn: forall m k : nat, nat_min n (nat_min m k) = nat_min (nat_min n m) k
nat_min n.+1 (nat_min m.+1 k.+1) =
nat_min (nat_min n.+1 m.+1) k.+1
  by apply (ap S), IHn.
Defined.

(** ** More theory of comparison predicates *)

(** *** Addition lemmas *)

(** The second summand is less than or equal to the sum. *)
Instance leq_add_l n m : n <= m + n.n, m: nat
n <= m + n
Proof.n, m: nat
n <= m + n
  simple_induction m m IH.n: nat
n <= 0 + n
n, m: nat
IH: n <= m + n
n <= m.+1 + n
  -n: nat
n <= 0 + n exact (leq_refl n).
  -n, m: nat
IH: n <= m + n
n <= m.+1 + n exact (leq_succ_r IH).
Defined.

(** The first summand is less than or equal to the sum. *)
Instance leq_add_r n m : n <= n + m.n, m: nat
n <= n + m
Proof.n, m: nat
n <= n + m
  simple_induction n n IHn.m: nat
0 <= 0 + m
m, n: nat
IHn: n <= n + m
n.+1 <= n.+1 + m
  -m: nat
0 <= 0 + m exact (leq_zero_l m).
  -m, n: nat
IHn: n <= n + m
n.+1 <= n.+1 + m exact (leq_succ IHn).
Defined.

(** *** Multiplication lemmas *)

(** The second multiplicand is less than or equal to the product. *)
Instance leq_mul_l n m l : l < m -> n <= m * n.n, m, l: nat
l < m -> n <= m * n
Proof.n, m, l: nat
l < m -> n <= m * n
  intros H; induction H; exact _.
Defined.

(** The first multiplicand is less than or equal to the product. *)
Instance leq_mul_r n m l : l < m -> n <= n * m.n, m, l: nat
l < m -> n <= n * m
Proof.n, m, l: nat
l < m -> n <= n * m
  rewrite nat_mul_comm; exact _.
Defined.

(** ** Eliminating positive assumptions *)

(** Sometimes we want to prove a predicate which assumes that [0 < x]. In that case, it suffices to prove it for [x.+1] instead. *)
Definition gt_zero_ind (P : nat -> Type)
  (H : forall x, P x.+1)
  : forall x (l : 0 < x), P x.P: nat -> Type
H: forall x : nat, P x.+1
forall x : nat, 0 < x -> P x
Proof.P: nat -> Type
H: forall x : nat, P x.+1
forall x : nat, 0 < x -> P x
  intros x l.P: nat -> Type
H: forall x : nat, P x.+1
x: nat
l: 0 < x
P x
  destruct x.P: nat -> Type
H: forall x : nat, P x.+1
l: 0 < 0
P 0
P: nat -> Type
H: forall x : nat, P x.+1
x: nat
l: 0 < x.+1
P x.+1
  1: contradiction (lt_irrefl _ l).P: nat -> Type
H: forall x : nat, P x.+1
x: nat
l: 0 < x.+1
P x.+1
  apply H.
Defined.

(** Alternative Characterizations of [<=] *)

(** [n <= m] is equivalent to [(n < m) + (n = m)]. This justifies the name "less than or equal to". Note that it is not immediately obvious that the latter type is a hprop. *)
Definition equiv_leq_lt_or_eq {n m} : (n <= m) <~> (n < m) + (n = m).n, m: nat
n <= m <~> (n < m) + (n = m)
Proof.n, m: nat
n <= m <~> (n < m) + (n = m)
  srapply equiv_iff_hprop.n, m: nat
IsHProp ((n < m) + (n = m))
n, m: nat
n <= m -> (n < m) + (n = m)
n, m: nat
(n < m) + (n = m) -> n <= m
  -n, m: nat
IsHProp ((n < m) + (n = m)) napply ishprop_sum.n, m: nat
IsHProp (n < m)
n, m: nat
IsHProp (n = m)
n, m: nat
n < m -> n = m -> Empty
    1,2: exact _.n, m: nat
n < m -> n = m -> Empty
    intros H1 p; destruct p.n: nat
H1: n < n
Empty
    contradiction (lt_irrefl _ _).
  -n, m: nat
n <= m -> (n < m) + (n = m) intro l; induction l.n: nat
((n < n) + (n = n))%type
n, m: nat
l: n <= m
IHl: ((n < m) + (n = m))%type
((n < m.+1) + (n = m.+1))%type
    +n: nat
((n < n) + (n = n))%type by right.
    +n, m: nat
l: n <= m
IHl: ((n < m) + (n = m))%type
((n < m.+1) + (n = m.+1))%type left; exact (leq_succ l).
  -n, m: nat
(n < m) + (n = m) -> n <= m intros [l|p].n, m: nat
l: n < m
n <= m
n, m: nat
p: n = m
n <= m
    +n, m: nat
l: n < m
n <= m exact (leq_succ_l l).
    +n, m: nat
p: n = m
n <= m destruct p.n: nat
n <= n
      exact (leq_refl _).
Defined.

(** Here is an alternative characterization of [<=] in terms of an existence predicate and addition. *)
Definition equiv_leq_add n m : n <= m <~> exists k, k + n = m.n, m: nat
n <= m <~> {k : nat & k + n = m}
Proof.n, m: nat
n <= m <~> {k : nat & k + n = m}
  srapply equiv_iff_hprop.n, m: nat
IsHProp {k : nat & k + n = m}
n, m: nat
n <= m -> {k : nat & k + n = m}
n, m: nat
{k : nat & k + n = m} -> n <= m
  -n, m: nat
IsHProp {k : nat & k + n = m} apply hprop_allpath.n, m: nat
forall x y : {k : nat & k + n = m}, x = y
    intros [x p] [y q].n, m, x: nat
p: x + n = m
y: nat
q: y + n = m
(x; p) = (y; q)
    pose (r := nat_moveL_nV _ p @ (nat_moveL_nV _ q)^).n, m, x: nat
p: x + n = m
y: nat
q: y + n = m
r:= nat_moveL_nV n p @ (nat_moveL_nV n q)^: x = y
(x; p) = (y; q)
    destruct r.n, m, x: nat
p, q: x + n = m
(x; p) = (x; q)
    apply ap.n, m, x: nat
p, q: x + n = m
p = q
    apply path_ishprop.
  -n, m: nat
n <= m -> {k : nat & k + n = m} intros p.n, m: nat
p: n <= m
{k : nat & k + n = m}
    exists (m - n).n, m: nat
p: n <= m
m - n + n = m
    apply nat_add_sub_l_cancel, p.
  -n, m: nat
{k : nat & k + n = m} -> n <= m intros [k p].n, m, k: nat
p: k + n = m
n <= m
    destruct p.n, k: nat
n <= k + n
    apply leq_add_l.
Defined.

(** *** Dichotomy of [<=] *)

Definition leq_dichotomy m n : (m <= n) + (m > n).m, n: nat
((m <= n) + (m > n))%type
Proof.m, n: nat
((m <= n) + (m > n))%type
  induction m as [|m IHm] in n |- *.n: nat
((0 <= n) + (0 > n))%type
m, n: nat
IHm: forall n : nat, (m <= n) + (m > n)
((m.+1 <= n) + (m.+1 > n))%type
  1: left; exact _.m, n: nat
IHm: forall n : nat, (m <= n) + (m > n)
((m.+1 <= n) + (m.+1 > n))%type
  destruct n.m: nat
IHm: forall n : nat, (m <= n) + (m > n)
((m.+1 <= 0) + (m.+1 > 0))%type
m, n: nat
IHm: forall n : nat, (m <= n) + (m > n)
((m.+1 <= n.+1) + (m.+1 > n.+1))%type
  1: right; exact _.m, n: nat
IHm: forall n : nat, (m <= n) + (m > n)
((m.+1 <= n.+1) + (m.+1 > n.+1))%type
  destruct (IHm n).m, n: nat
IHm: forall n : nat, (m <= n) + (m > n)
l: m <= n
((m.+1 <= n.+1) + (m.+1 > n.+1))%type
m, n: nat
IHm: forall n : nat, (m <= n) + (m > n)
g: m > n
((m.+1 <= n.+1) + (m.+1 > n.+1))%type
  1: left; exact _.m, n: nat
IHm: forall n : nat, (m <= n) + (m > n)
g: m > n
((m.+1 <= n.+1) + (m.+1 > n.+1))%type
  1: right; exact _.
Defined.

(** A variant. *)
Definition leq_succ_dichotomy {n m : nat} (l : m <= n.+1) : (m = n.+1) + (m <= n).n, m: nat
l: m <= n.+1
((m = n.+1) + (m <= n))%type
Proof.n, m: nat
l: m <= n.+1
((m = n.+1) + (m <= n))%type
  inversion l.n, m: nat
l: m <= n.+1
X: m = n.+1
((n.+1 = n.+1) + (n.+1 <= n))%type
n, m: nat
l: m <= n.+1
m0: nat
H: m <= n
X0: m0 = n
((m = n.+1) + (m <= n))%type
  -n, m: nat
l: m <= n.+1
X: m = n.+1
((n.+1 = n.+1) + (n.+1 <= n))%type left; reflexivity.
  -n, m: nat
l: m <= n.+1
m0: nat
H: m <= n
X0: m0 = n
((m = n.+1) + (m <= n))%type right; assumption.
Defined.

(** *** Trichotomy *)

(** Any two natural numbers are either equal, less than, or greater than each other. *)
Definition nat_trichotomy m n : (m < n) + (m = n) + (m > n).m, n: nat
((m < n) + (m = n) + (m > n))%type
Proof.m, n: nat
((m < n) + (m = n) + (m > n))%type
  generalize (leq_dichotomy m n).m, n: nat
(m <= n) + (m > n) -> (m < n) + (m = n) + (m > n)
  snapply (functor_sum _ idmap).m, n: nat
m <= n -> (m < n) + (m = n)
  exact equiv_leq_lt_or_eq.
Defined.

(** *** Negation lemmas *)

(** There are various lemmas we can state about negating the comparison operators on [nat]. To aid readability, we opt to keep the order of the variables in each statement consistent. *)

Definition geq_iff_not_lt {n m} : ~(n < m) <-> n >= m.n, m: nat
~ (n < m) <-> n >= m
Proof.n, m: nat
~ (n < m) <-> n >= m
  split.n, m: nat
~ (n < m) -> n >= m
n, m: nat
n >= m -> ~ (n < m)
  -n, m: nat
~ (n < m) -> n >= m intro; by destruct (leq_dichotomy m n).
  -n, m: nat
n >= m -> ~ (n < m) intros ? ?; contradiction (lt_irrefl n); exact _.
Defined.

Definition gt_iff_not_leq {n m} : ~(n <= m) <-> n > m.n, m: nat
~ (n <= m) <-> n > m
Proof.n, m: nat
~ (n <= m) <-> n > m
  split.n, m: nat
~ (n <= m) -> n > m
n, m: nat
n > m -> ~ (n <= m)
  -n, m: nat
~ (n <= m) -> n > m intro; by destruct (leq_dichotomy n m).
  -n, m: nat
n > m -> ~ (n <= m) intros ? ?; contradiction (lt_irrefl m); exact _.
Defined.

Definition leq_iff_not_gt {n m} : ~(n > m) <-> n <= m
  := geq_iff_not_lt.

Definition lt_iff_not_geq {n m} : ~(n >= m) <-> n < m
  := gt_iff_not_leq.

(** *** Dichotomy of [<>] *)

(** The inequality of natural numbers is equivalent to [n < m] or [n > m]. This could be an equivalence; however, one of the sections requires [Funext] since we are comparing two inequality proofs. It is therefore more useful to keep it as a biimplication. Note that this is a negated version of antisymmetry of [<=]. *)
Definition neq_iff_lt_or_gt {n m} : n <> m <-> (n < m) + (n > m).n, m: nat
n <> m <-> (n < m) + (n > m)
Proof.n, m: nat
n <> m <-> (n < m) + (n > m)
  split.n, m: nat
n <> m -> (n < m) + (n > m)
n, m: nat
(n < m) + (n > m) -> n <> m
  -n, m: nat
n <> m -> (n < m) + (n > m) intros diseq.n, m: nat
diseq: n <> m
((n < m) + (n > m))%type
    destruct (dec (n < m)) as [| a]; [ by left |].n, m: nat
diseq: n <> m
a: ~ (n < m)
((n < m) + (n > m))%type
    apply geq_iff_not_lt in a.n, m: nat
diseq: n <> m
a: n >= m
((n < m) + (n > m))%type
    apply equiv_leq_lt_or_eq in a.n, m: nat
diseq: n <> m
a: ((m < n) + (m = n))%type
((n < m) + (n > m))%type
    destruct a as [lt | eq].n, m: nat
diseq: n <> m
lt: m < n
((n < m) + (n > m))%type
n, m: nat
diseq: n <> m
eq: m = n
((n < m) + (n > m))%type
    1: by right.n, m: nat
diseq: n <> m
eq: m = n
((n < m) + (n > m))%type
    symmetry in eq.n, m: nat
diseq: n <> m
eq: n = m
((n < m) + (n > m))%type
    contradiction.
  -n, m: nat
(n < m) + (n > m) -> n <> m intros [H' | H'] nq; destruct nq; exact (lt_irrefl _ H').
Defined.

(** ** Arithmetic relations between [trunc_index] and [nat]. *)

Definition trunc_index_add_nat_add {n : nat}: trunc_index_add n n = n.+1 + n.+1.n: nat
(n +2+ n)%trunc = n.+1 + n.+1
Proof.n: nat
(n +2+ n)%trunc = n.+1 + n.+1
  induction n as [|n IHn].(0%nat +2+ 0%nat)%trunc = 1 + 1
n: nat
IHn: (n +2+ n)%trunc = n.+1 + n.+1
(n.+1%nat +2+ n.+1%nat)%trunc = n.+2 + n.+2
  1: reflexivity.n: nat
IHn: (n +2+ n)%trunc = n.+1 + n.+1
(n.+1%nat +2+ n.+1%nat)%trunc = n.+2 + n.+2
  lhs napply trunc_index_add_succ.n: nat
IHn: (n +2+ n)%trunc = n.+1 + n.+1
(n.+1%nat +2+ (trunc_index_inc (-2) n.+1).+1).+1%trunc =
n.+2 + n.+2
  rhs napply (ap nat_to_trunc_index).n: nat
IHn: (n +2+ n)%trunc = n.+1 + n.+1
(n.+1%nat +2+ (trunc_index_inc (-2) n.+1).+1).+1%trunc =
?Goal
n: nat
IHn: (n +2+ n)%trunc = n.+1 + n.+1
n.+2 + n.+2 = ?Goal
  2: napply nat_add_succ_r.n: nat
IHn: (n +2+ n)%trunc = n.+1 + n.+1
(n.+1%nat +2+ (trunc_index_inc (-2) n.+1).+1).+1%trunc =
(n.+2 + n.+1).+1
  exact (ap (fun x => x.+2%trunc) IHn).
Defined.

(** *** Subtraction *)

Instance leq_sub_add_l n m : n <= n - m + m.n, m: nat
n <= n - m + m
Proof.n, m: nat
n <= n - m + m
  destruct (@leq_dichotomy m n) as [l | g].n, m: nat
l: m <= n
n <= n - m + m
n, m: nat
g: m > n
n <= n - m + m
  -n, m: nat
l: m <= n
n <= n - m + m by rewrite nat_add_sub_l_cancel.
  -n, m: nat
g: m > n
n <= n - m + m apply leq_lt in g.n, m: nat
g: n <= m
n <= n - m + m
    by destruct (equiv_nat_sub_leq _)^.
Defined.

Instance leq_sub_add_r n m : n <= m + (n - m).n, m: nat
n <= m + (n - m)
Proof.n, m: nat
n <= m + (n - m)
  rewrite nat_add_comm; exact _.
Defined.

(** A number being less than another is equivalent to their difference being greater than zero. *)
Definition equiv_lt_lt_sub n m : m < n <~> 0 < n - m.n, m: nat
m < n <~> 0 < n - m
Proof.n, m: nat
m < n <~> 0 < n - m
  induction n as [|n IHn] in m |- *.m: nat
m < 0 <~> 0 < 0 - m
n, m: nat
IHn: forall m : nat, m < n <~> 0 < n - m
m < n.+1 <~> 0 < n.+1 - m
  1: srapply equiv_iff_hprop; intro; contradiction (not_lt_zero_r _ _).n, m: nat
IHn: forall m : nat, m < n <~> 0 < n - m
m < n.+1 <~> 0 < n.+1 - m
  destruct m; only 1: reflexivity.n, m: nat
IHn: forall m : nat, m < n <~> 0 < n - m
m.+1 < n.+1 <~> 0 < n.+1 - m.+1
  nrefine (IHn m oE _).n, m: nat
IHn: forall m : nat, m < n <~> 0 < n - m
m.+1 < n.+1 <~> m < n
  srapply equiv_iff_hprop.
Defined.

(** *** Monotonicity of addition *)

(** TODO: use [OrderPreserving] from canonical_names *)

(** Addition on the left is monotone. *)
Definition nat_add_l_monotone {n m} k
  : n <= m -> k + n <= k + m.n, m, k: nat
n <= m -> k + n <= k + m
Proof.n, m, k: nat
n <= m -> k + n <= k + m
  intros H; induction k; exact _.
Defined.
Hint Immediate nat_add_l_monotone : typeclass_instances.

(** Addition on the right is monotone. *)
Definition nat_add_r_monotone {n m} k
  : n <= m -> n + k <= m + k.n, m, k: nat
n <= m -> n + k <= m + k
Proof.n, m, k: nat
n <= m -> n + k <= m + k
  intros H; rewrite 2 (nat_add_comm _ k); exact _.
Defined.
Hint Immediate nat_add_r_monotone : typeclass_instances.

(** Addition is monotone in both arguments. (This makes [+] a bifunctor when treating [nat] as a category (as a preorder)). *)
Definition nat_add_monotone {n n' m m'}
  : n <= m -> n' <= m' -> n + n' <= m + m'.n, n', m, m': nat
n <= m -> n' <= m' -> n + n' <= m + m'
Proof.n, n', m, m': nat
n <= m -> n' <= m' -> n + n' <= m + m'
  intros H1 H2; induction H1; exact _.
Defined.
Hint Immediate nat_add_monotone : typeclass_instances.

(** *** Strict monotonicity of addition *)

(** [nat_succ] is strictly monotone. *)
Instance lt_succ {n m} : n < m -> n.+1 < m.+1 := _.

Instance lt_succ_r {n m} : n < m -> n < m.+1 | 100 := _.

(** Addition on the left is strictly monotone. *)
Definition nat_add_l_strictly_monotone {n m} k
  : n < m -> k + n < k + m.n, m, k: nat
n < m -> k + n < k + m
Proof.n, m, k: nat
n < m -> k + n < k + m
  intros H; induction k; exact _.
Defined.
Hint Immediate nat_add_l_strictly_monotone : typeclass_instances.

(** Addition on the right is strictly monotone. *)
Definition nat_add_r_strictly_monotone {n m} k
  : n < m -> n + k < m + k.n, m, k: nat
n < m -> n + k < m + k
Proof.n, m, k: nat
n < m -> n + k < m + k
  intros H; rewrite 2 (nat_add_comm _ k); exact _.
Defined.
Hint Immediate nat_add_r_strictly_monotone : typeclass_instances.

(** Addition is strictly monotone in both arguments. *)
Definition nat_add_strictly_monotone {n n' m m'}
  : n < m -> n' < m' -> n + n' < m + m'.n, n', m, m': nat
n < m -> n' < m' -> n + n' < m + m'
Proof.n, n', m, m': nat
n < m -> n' < m' -> n + n' < m + m'
  intros H1 H2; induction H1; exact _.
Defined.
Hint Immediate nat_add_strictly_monotone : typeclass_instances.

(** *** Monotonicity of multiplication *)

(** Multiplication on the left is monotone. *)
Definition nat_mul_l_monotone {n m} k
  : n <= m -> k * n <= k * m.n, m, k: nat
n <= m -> k * n <= k * m
Proof.n, m, k: nat
n <= m -> k * n <= k * m
  intros H; induction k; exact _.
Defined.
Hint Immediate nat_mul_l_monotone : typeclass_instances.

(** Multiplication on the right is monotone. *)
Definition nat_mul_r_monotone {n m} k
  : n <= m -> n * k <= m * k.n, m, k: nat
n <= m -> n * k <= m * k
Proof.n, m, k: nat
n <= m -> n * k <= m * k
  intros H; rewrite 2 (nat_mul_comm _ k); exact _.
Defined.
Hint Immediate nat_mul_r_monotone : typeclass_instances.

(** Multiplication is monotone in both arguments. *)
Definition nat_mul_monotone {n n' m m'}
  : n <= m -> n' <= m' -> n * n' <= m * m'.n, n', m, m': nat
n <= m -> n' <= m' -> n * n' <= m * m'
Proof.n, n', m, m': nat
n <= m -> n' <= m' -> n * n' <= m * m'
  intros H1 H2; induction H1; exact _.
Defined.
Hint Immediate nat_mul_monotone : typeclass_instances.

(** *** Strict monotonicity of multiplication *)

(** Multiplication on the left by a positive number is strictly monotone. *)
Definition nat_mul_l_strictly_monotone {n m l} k
  : l < k -> n < m -> k * n < k * m.n, m, l, k: nat
l < k -> n < m -> k * n < k * m
Proof.n, m, l, k: nat
l < k -> n < m -> k * n < k * m
  destruct k.n, m, l: nat
l < 0 -> n < m -> 0 * n < 0 * m
n, m, l, k: nat
l < k.+1 -> n < m -> k.+1 * n < k.+1 * m
  1: intro; contradiction (not_lt_zero_r _ H).n, m, l, k: nat
l < k.+1 -> n < m -> k.+1 * n < k.+1 * m
  intros _ H; induction k as [|k IHk] in |- *; exact _.
Defined.
Hint Immediate nat_mul_l_strictly_monotone : typeclass_instances.

(** Multiplication on the right by a positive number is strictly monotone. *)
Definition nat_mul_r_strictly_monotone {n m l} k
  : l < k -> n < m -> n * k < m * k.n, m, l, k: nat
l < k -> n < m -> n * k < m * k
Proof.n, m, l, k: nat
l < k -> n < m -> n * k < m * k
  intros ? H; rewrite 2 (nat_mul_comm _ k); exact _.
Defined.
Hint Immediate nat_mul_r_strictly_monotone : typeclass_instances.

(** Multiplication is strictly monotone in both arguments. *)
Definition nat_mul_strictly_monotone {n n' m m'}
  : n < m -> n' < m' -> n * n' < m * m'.n, n', m, m': nat
n < m -> n' < m' -> n * n' < m * m'
Proof.n, n', m, m': nat
n < m -> n' < m' -> n * n' < m * m'
  intros H1 H2.n, n', m, m': nat
H1: n < m
H2: n' < m'
n * n' < m * m'
  napply (lt_leq_lt_trans (m:=n * m')).n, n', m, m': nat
H1: n < m
H2: n' < m'
n * n' <= n * m'
n, n', m, m': nat
H1: n < m
H2: n' < m'
n * m' < m * m'
  1: rapply nat_mul_l_monotone.n, n', m, m': nat
H1: n < m
H2: n' < m'
n * m' < m * m'
  rapply nat_mul_r_strictly_monotone.
Defined.
Hint Immediate nat_mul_strictly_monotone : typeclass_instances.

(** *** Order-reflection *)

(** Addition on the left is order-reflecting. *)
Definition leq_reflects_add_l {n m} k : k + n <= k + m -> n <= m.n, m, k: nat
k + n <= k + m -> n <= m
Proof.n, m, k: nat
k + n <= k + m -> n <= m
  intros H; induction k; exact _.
Defined.

(** Addition on the right is order-reflecting. *)
Definition leq_reflects_add_r {n m} k : n + k <= m + k -> n <= m.n, m, k: nat
n + k <= m + k -> n <= m
Proof.n, m, k: nat
n + k <= m + k -> n <= m
  rewrite 2 (nat_add_comm _ k); napply leq_reflects_add_l.
Defined.

(** Addition on the left is strictly order-reflecting. *)
Definition lt_reflects_add_l {n m} k : k + n < k + m -> n < m.n, m, k: nat
k + n < k + m -> n < m
Proof.n, m, k: nat
k + n < k + m -> n < m
  intros H; induction k; exact _.
Defined.

(** Addition on the right is strictly order-reflecting. *)
Definition lt_reflects_add_r {n m} k : n + k < m + k -> n < m.n, m, k: nat
n + k < m + k -> n < m
Proof.n, m, k: nat
n + k < m + k -> n < m
  rewrite 2 (nat_add_comm _ k); napply lt_reflects_add_l.
Defined.

(** ** Further properties of subtraction *)

Instance leq_sub_l n m : n - m <= n.n, m: nat
n - m <= n
Proof.n, m: nat
n - m <= n
  apply equiv_nat_sub_leq.n, m: nat
n - m - n = 0
  rewrite nat_sub_comm_r.n, m: nat
n - n - m = 0
  rewrite nat_sub_cancel.n, m: nat
0 - m = 0
  apply nat_sub_zero_l.
Defined.

(** Subtracting from a successor is the successor of subtracting from the original number, as long as the amount being subtracted is less than or equal to the original number. *)
Definition nat_sub_succ_l n m : m <= n -> n.+1 - m = (n - m).+1.n, m: nat
m <= n -> n.+1 - m = (n - m).+1
Proof.n, m: nat
m <= n -> n.+1 - m = (n - m).+1
  intros H.n, m: nat
H: m <= n
n.+1 - m = (n - m).+1
  induction m as [|m IHm] in n, H |- *.n: nat
H: 0 <= n
n.+1 - 0 = (n - 0).+1
n, m: nat
H: m.+1 <= n
IHm: forall n : nat, m <= n -> n.+1 - m = (n - m).+1
n.+1 - m.+1 = (n - m.+1).+1
  -n: nat
H: 0 <= n
n.+1 - 0 = (n - 0).+1 by rewrite 2 nat_sub_zero_r.
  -n, m: nat
H: m.+1 <= n
IHm: forall n : nat, m <= n -> n.+1 - m = (n - m).+1
n.+1 - m.+1 = (n - m.+1).+1 simpl.n, m: nat
H: m.+1 <= n
IHm: forall n : nat, m <= n -> n.+1 - m = (n - m).+1
n - m = (n - m.+1).+1
    rewrite nat_sub_succ_r.n, m: nat
H: m.+1 <= n
IHm: forall n : nat, m <= n -> n.+1 - m = (n - m).+1
n - m = (nat_pred (n - m)).+1
    symmetry.n, m: nat
H: m.+1 <= n
IHm: forall n : nat, m <= n -> n.+1 - m = (n - m).+1
(nat_pred (n - m)).+1 = n - m
    apply nat_succ_pred.n, m: nat
H: m.+1 <= n
IHm: forall n : nat, m <= n -> n.+1 - m = (n - m).+1
0 < n - m
    by apply equiv_lt_lt_sub.
Defined.

(** Under certain conditions, subtracting a predecessor is the successor of the subtraction. *)
Definition nat_sub_pred_r n m : 0 < m -> m < n -> n - nat_pred m = (n - m).+1.n, m: nat
0 < m -> m < n -> n - nat_pred m = (n - m).+1
Proof.n, m: nat
0 < m -> m < n -> n - nat_pred m = (n - m).+1
  revert m; snapply gt_zero_ind.n: nat
forall x : nat,
(fun x0 : nat =>
 x0 < n -> n - nat_pred x0 = (n - x0).+1) x.+1
  intros m H1.n, m: nat
H1: m.+1 < n
n - nat_pred m.+1 = (n - m.+1).+1
  rewrite nat_sub_succ_r.n, m: nat
H1: m.+1 < n
n - nat_pred m.+1 = (nat_pred (n - m)).+1
  rewrite nat_succ_pred.n, m: nat
H1: m.+1 < n
n - nat_pred m.+1 = n - m
n, m: nat
H1: m.+1 < n
0 < n - m
  1: reflexivity.n, m: nat
H1: m.+1 < n
0 < n - m
  apply equiv_lt_lt_sub.n, m: nat
H1: m.+1 < n
m < n
  exact (lt_trans _ H1).
Defined.

(** Subtracting from a sum is the sum of subtracting from the second summand. *)
Definition nat_sub_l_add_r m n k
  : k <= m -> (n + m) - k = n + (m - k).m, n, k: nat
k <= m -> n + m - k = n + (m - k)
Proof.m, n, k: nat
k <= m -> n + m - k = n + (m - k)
  intros H; induction n as [|n IHn] in |- *.m, k: nat
H: k <= m
0 + m - k = 0 + (m - k)
m, n, k: nat
H: k <= m
IHn: n + m - k = n + (m - k)
n.+1 + m - k = n.+1 + (m - k)
  -m, k: nat
H: k <= m
0 + m - k = 0 + (m - k) reflexivity.
  -m, n, k: nat
H: k <= m
IHn: n + m - k = n + (m - k)
n.+1 + m - k = n.+1 + (m - k) change (?n.+1 + ?m) with (n + m).+1.m, n, k: nat
H: k <= m
IHn: n + m - k = n + (m - k)
(n + m).+1 - k = (n + (m - k)).+1
    lhs napply nat_sub_succ_l.m, n, k: nat
H: k <= m
IHn: n + m - k = n + (m - k)
k <= n + m
m, n, k: nat
H: k <= m
IHn: n + m - k = n + (m - k)
(n + m - k).+1 = (n + (m - k)).+1
    2: exact (ap nat_succ IHn).m, n, k: nat
H: k <= m
IHn: n + m - k = n + (m - k)
k <= n + m
    exact _.
Defined.

(** Subtracting from a sum is the sum of subtracting from the first summand. *)
Definition nat_sub_l_add_l n m k
  : k <= n -> (n + m) - k = (n - k) + m.n, m, k: nat
k <= n -> n + m - k = n - k + m
Proof.n, m, k: nat
k <= n -> n + m - k = n - k + m
  intro l.n, m, k: nat
l: k <= n
n + m - k = n - k + m
  rewrite nat_add_comm.n, m, k: nat
l: k <= n
m + n - k = n - k + m
  lhs rapply nat_sub_l_add_r.n, m, k: nat
l: k <= n
m + (n - k) = n - k + m
  apply nat_add_comm.
Defined.

(** Subtracting a subtraction is the subtrahend. *)
Definition nat_sub_sub_cancel_r {n m} : n <= m -> m - (m - n) = n.n, m: nat
n <= m -> m - (m - n) = n
Proof.n, m: nat
n <= m -> m - (m - n) = n
  intros H; induction H.n: nat
n - (n - n) = n
n, m: nat
H: n <= m
IHleq: m - (m - n) = n
m.+1 - (m.+1 - n) = n
  -n: nat
n - (n - n) = n by rewrite nat_sub_cancel, nat_sub_zero_r.
  -n, m: nat
H: n <= m
IHleq: m - (m - n) = n
m.+1 - (m.+1 - n) = n rewrite (nat_sub_succ_l m n); only 2: exact _.n, m: nat
H: n <= m
IHleq: m - (m - n) = n
m.+1 - (m - n).+1 = n
    exact IHleq.
Defined.

(** Multiplication on the left distributes over subtraction. *)
Definition nat_dist_sub_l n m k
  : n * (m - k) = n * m - n * k.n, m, k: nat
n * (m - k) = n * m - n * k
Proof.n, m, k: nat
n * (m - k) = n * m - n * k
  induction n as [|n IHn] in m, k |- *.m, k: nat
0 * (m - k) = 0 * m - 0 * k
n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
n.+1 * (m - k) = n.+1 * m - n.+1 * k
  1: reflexivity.n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
n.+1 * (m - k) = n.+1 * m - n.+1 * k
  destruct (leq_dichotomy k m) as [l|r].n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
l: k <= m
n.+1 * (m - k) = n.+1 * m - n.+1 * k
n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
r: k > m
n.+1 * (m - k) = n.+1 * m - n.+1 * k
  -n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
l: k <= m
n.+1 * (m - k) = n.+1 * m - n.+1 * k simpl; rewrite IHn, <- nat_sub_l_add_r, <- nat_sub_l_add_l,
      nat_sub_r_add; trivial; exact _.
  -n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
r: k > m
n.+1 * (m - k) = n.+1 * m - n.+1 * k apply leq_lt in r.n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
r: m <= k
n.+1 * (m - k) = n.+1 * m - n.+1 * k
    apply equiv_nat_sub_leq in r.n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
r: m - k = 0
n.+1 * (m - k) = n.+1 * m - n.+1 * k
    rewrite r.n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
r: m - k = 0
n.+1 * 0 = n.+1 * m - n.+1 * k
    rewrite nat_mul_zero_r.n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
r: m - k = 0
0 = n.+1 * m - n.+1 * k
    symmetry.n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
r: m - k = 0
n.+1 * m - n.+1 * k = 0
    apply equiv_nat_sub_leq.n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
r: m - k = 0
n.+1 * m <= n.+1 * k
    apply nat_mul_l_monotone.n, m, k: nat
IHn: forall m k : nat, n * (m - k) = n * m - n * k
r: m - k = 0
m <= k
    by apply equiv_nat_sub_leq.
Defined.

(** Multiplication on the right distributes over subtraction. *)
Definition nat_dist_sub_r n m k
  : (n - m) * k = n * k - m * k.n, m, k: nat
(n - m) * k = n * k - m * k
Proof.n, m, k: nat
(n - m) * k = n * k - m * k
  rewrite 3 (nat_mul_comm _ k).n, m, k: nat
k * (n - m) = k * n - k * m
  apply nat_dist_sub_l.
Defined.

(** *** Monotonicity of subtraction *)

(** Subtraction is monotone in the left argument. *)
Definition nat_sub_monotone_l {n m} k : n <= m -> n - k <= m - k.n, m, k: nat
n <= m -> n - k <= m - k
Proof.n, m, k: nat
n <= m -> n - k <= m - k
  intros H.n, m, k: nat
H: n <= m
n - k <= m - k
  destruct (leq_dichotomy k n) as [l|r].n, m, k: nat
H: n <= m
l: k <= n
n - k <= m - k
n, m, k: nat
H: n <= m
r: k > n
n - k <= m - k
  -n, m, k: nat
H: n <= m
l: k <= n
n - k <= m - k apply (leq_reflects_add_l k).n, m, k: nat
H: n <= m
l: k <= n
k + (n - k) <= k + (m - k)
    rewrite 2 nat_add_sub_r_cancel.n, m, k: nat
H: n <= m
l: k <= n
n <= m
n, m, k: nat
H: n <= m
l: k <= n
k <= m
n, m, k: nat
H: n <= m
l: k <= n
k <= n
    +n, m, k: nat
H: n <= m
l: k <= n
n <= m exact H.
    +n, m, k: nat
H: n <= m
l: k <= n
k <= m rapply leq_trans.
    +n, m, k: nat
H: n <= m
l: k <= n
k <= n exact l.
  -n, m, k: nat
H: n <= m
r: k > n
n - k <= m - k apply leq_succ_l in r.n, m, k: nat
H: n <= m
r: n <= k
n - k <= m - k
    apply equiv_nat_sub_leq in r.n, m, k: nat
H: n <= m
r: n - k = 0
n - k <= m - k
    destruct r^.n, m, k: nat
H: n <= m
r: 0 = 0
0 <= m - k
    exact _.
Defined.
Hint Immediate nat_sub_monotone_l : typeclass_instances.

(** Subtraction is contravariantly monotone in the right argument. *)
Definition nat_sub_monotone_r {n m} k : n <= m -> k - m <= k - n.n, m, k: nat
n <= m -> k - m <= k - n
Proof.n, m, k: nat
n <= m -> k - m <= k - n
  intros H.n, m, k: nat
H: n <= m
k - m <= k - n
  induction k.n, m: nat
H: n <= m
0 - m <= 0 - n
n, m, k: nat
H: n <= m
IHk: k - m <= k - n
k.+1 - m <= k.+1 - n
  -n, m: nat
H: n <= m
0 - m <= 0 - n by rewrite nat_sub_zero_l.
  -n, m, k: nat
H: n <= m
IHk: k - m <= k - n
k.+1 - m <= k.+1 - n destruct (leq_dichotomy m k) as [l|r].n, m, k: nat
H: n <= m
IHk: k - m <= k - n
l: m <= k
k.+1 - m <= k.+1 - n
n, m, k: nat
H: n <= m
IHk: k - m <= k - n
r: m > k
k.+1 - m <= k.+1 - n
    +n, m, k: nat
H: n <= m
IHk: k - m <= k - n
l: m <= k
k.+1 - m <= k.+1 - n rewrite 2 nat_sub_succ_l; exact _.
    +n, m, k: nat
H: n <= m
IHk: k - m <= k - n
r: m > k
k.+1 - m <= k.+1 - n apply equiv_nat_sub_leq in r.n, m, k: nat
H: n <= m
IHk: k - m <= k - n
r: k.+1 - m = 0
k.+1 - m <= k.+1 - n
      destruct r^.n, m, k: nat
H: n <= m
IHk: k - m <= k - n
r: 0 = 0
0 <= k.+1 - n
      exact _.
Defined.
Hint Immediate nat_sub_monotone_r : typeclass_instances.

(** *** Order-reflection lemmas *)

(** Subtraction reflects [<=] in the left argument. *)
Definition leq_reflects_sub_l {n m} k : k <= m -> n - k <= m - k -> n <= m.n, m, k: nat
k <= m -> n - k <= m - k -> n <= m
Proof.n, m, k: nat
k <= m -> n - k <= m - k -> n <= m
  intros ineq1 ineq2.n, m, k: nat
ineq1: k <= m
ineq2: n - k <= m - k
n <= m
  apply (nat_add_r_monotone k) in ineq2.n, m, k: nat
ineq1: k <= m
ineq2: n - k + k <= m - k + k
n <= m
  apply (@leq_trans _ (n - k + k) _ (leq_sub_add_l _ _)).n, m, k: nat
ineq1: k <= m
ineq2: n - k + k <= m - k + k
n - k + k <= m
  apply (@leq_trans _ (m - k + k) _ _).n, m, k: nat
ineq1: k <= m
ineq2: n - k + k <= m - k + k
m - k + k <= m
  by rewrite nat_add_sub_l_cancel.
Defined.

(** Subtraction reflects [<=] in the right argument contravariantly. *)
Definition leq_reflects_sub_r {n m} k
  : m <= k -> n <= k -> k - n <= k - m -> m <= n.n, m, k: nat
m <= k -> n <= k -> k - n <= k - m -> m <= n
Proof.n, m, k: nat
m <= k -> n <= k -> k - n <= k - m -> m <= n
  intros H1 H2 H3.n, m, k: nat
H1: m <= k
H2: n <= k
H3: k - n <= k - m
m <= n
  apply (nat_sub_monotone_r k) in H3.n, m, k: nat
H1: m <= k
H2: n <= k
H3: k - (k - m) <= k - (k - n)
m <= n
  rewrite 2 nat_sub_sub_cancel_r in H3; exact _.
Defined.

(** *** Movement lemmas *)

(** Given an inequality [n < m] we can move around a summand or subtrahend [k] from either side. *)

Definition leq_moveL_Mn {n m} k : n - k <= m -> n <= k + m.n, m, k: nat
n - k <= m -> n <= k + m
Proof.n, m, k: nat
n - k <= m -> n <= k + m
  intros H.n, m, k: nat
H: n - k <= m
n <= k + m
  rewrite nat_add_comm.n, m, k: nat
H: n - k <= m
n <= m + k
  apply (nat_add_r_monotone k) in H.n, m, k: nat
H: n - k + k <= m + k
n <= m + k
  rapply leq_trans.
Defined.

Definition leq_moveL_nM {n m} k : n - k <= m -> n <= m + k.n, m, k: nat
n - k <= m -> n <= m + k
Proof.n, m, k: nat
n - k <= m -> n <= m + k
  rewrite nat_add_comm.n, m, k: nat
n - k <= m -> n <= k + m
  apply leq_moveL_Mn.
Defined.

Definition leq_moveR_Mn {n m} k : k <= m -> n <= m - k -> k + n <= m.n, m, k: nat
k <= m -> n <= m - k -> k + n <= m
Proof.n, m, k: nat
k <= m -> n <= m - k -> k + n <= m
  intros H1 H2.n, m, k: nat
H1: k <= m
H2: n <= m - k
k + n <= m
  rapply (leq_reflects_sub_l k).n, m, k: nat
H1: k <= m
H2: n <= m - k
k + n - k <= m - k
  by rewrite nat_add_sub_cancel_l.
Defined.

Definition leq_moveR_nM {n m} k : k <= m -> n <= m - k -> n + k <= m.n, m, k: nat
k <= m -> n <= m - k -> n + k <= m
Proof.n, m, k: nat
k <= m -> n <= m - k -> n + k <= m
  rewrite nat_add_comm.n, m, k: nat
k <= m -> n <= m - k -> k + n <= m
  apply leq_moveR_Mn.
Defined.

Definition leq_moveL_nV {n m} k : n + k <= m -> n <= m - k.n, m, k: nat
n + k <= m -> n <= m - k
Proof.n, m, k: nat
n + k <= m -> n <= m - k
  intros H.n, m, k: nat
H: n + k <= m
n <= m - k
  apply (leq_reflects_add_r k).n, m, k: nat
H: n + k <= m
n + k <= m - k + k
  rapply leq_trans.
Defined.

Definition leq_moveR_nV {n m} k : n <= m + k -> n - k <= m.n, m, k: nat
n <= m + k -> n - k <= m
Proof.n, m, k: nat
n <= m + k -> n - k <= m
  intros H.n, m, k: nat
H: n <= m + k
n - k <= m
  apply (nat_sub_monotone_l k) in H.n, m, k: nat
H: n - k <= m + k - k
n - k <= m
  by rewrite nat_add_sub_cancel_r in H.
Defined.

Definition lt_moveL_Mn {n m} k : n - k < m -> n < k + m.n, m, k: nat
n - k < m -> n < k + m
Proof.n, m, k: nat
n - k < m -> n < k + m
  intros H.n, m, k: nat
H: n - k < m
n < k + m
  apply (nat_add_l_strictly_monotone k) in H.n, m, k: nat
H: k + (n - k) < k + m
n < k + m
  rapply lt_leq_lt_trans.
Defined.

Definition lt_moveL_nM {n m} k : n - k < m -> n < m + k.n, m, k: nat
n - k < m -> n < m + k
Proof.n, m, k: nat
n - k < m -> n < m + k
  rewrite nat_add_comm.n, m, k: nat
n - k < m -> n < k + m
  apply lt_moveL_Mn.
Defined.

Definition lt_moveR_Mn {n m} k : k < m -> n < m - k -> k + n < m.n, m, k: nat
k < m -> n < m - k -> k + n < m
Proof.n, m, k: nat
k < m -> n < m - k -> k + n < m
  intros H1 H2.n, m, k: nat
H1: k < m
H2: n < m - k
k + n < m
  rewrite nat_add_comm.n, m, k: nat
H1: k < m
H2: n < m - k
n + k < m
  rapply (leq_moveR_nM (n:=n.+1) k).
Defined.

Definition lt_moveR_nM {n m} k : k < m -> n < m - k -> n + k < m.n, m, k: nat
k < m -> n < m - k -> n + k < m
Proof.n, m, k: nat
k < m -> n < m - k -> n + k < m
  rewrite nat_add_comm.n, m, k: nat
k < m -> n < m - k -> k + n < m
  apply lt_moveR_Mn.
Defined.

Definition lt_moveL_nV {n m} k : n + k < m -> n < m - k.n, m, k: nat
n + k < m -> n < m - k
Proof.n, m, k: nat
n + k < m -> n < m - k
  intros H.n, m, k: nat
H: n + k < m
n < m - k
  rapply leq_moveL_nV.
Defined.

Definition lt_moveR_nV {n m} k : k <= n -> n < k + m -> n - k < m.n, m, k: nat
k <= n -> n < k + m -> n - k < m
Proof.n, m, k: nat
k <= n -> n < k + m -> n - k < m
  intros H1 H2; unfold lt.n, m, k: nat
H1: k <= n
H2: n < k + m
(n - k).+1 <= m
  rewrite <- nat_sub_succ_l; only 2: exact _.n, m, k: nat
H1: k <= n
H2: n < k + m
n.+1 - k <= m
  rewrite <- (nat_add_sub_cancel_l m k).n, m, k: nat
H1: k <= n
H2: n < k + m
n.+1 - k <= k + m - k
  by apply nat_sub_monotone_l.
Defined.

(** ** Properties of powers *)

(** [0] to any power is [0] unless that power is [0] in which case it is [1]. *)
Definition nat_pow_zero_l@{} n : nat_pow 0 n = if dec (n = 0) then 1 else 0.n: nat
nat_pow 0 n = (if dec (n = 0) then 1 else 0)
Proof.n: nat
nat_pow 0 n = (if dec (n = 0) then 1 else 0)
  destruct n; reflexivity.
Defined.

(** Any number to the power of [0] is [1]. *)
Definition nat_pow_zero_r@{} n : nat_pow n 0 = 1
  := idpath.

(** [1] to any power is [1]. *)
Definition nat_pow_one_l@{} n : nat_pow 1 n = 1.n: nat
nat_pow 1 n = 1
Proof.n: nat
nat_pow 1 n = 1
  induction n as [|n IHn]; simpl.1 = 1
n: nat
IHn: nat_pow 1 n = 1
nat_pow 1 n + 0 = 1
  1: reflexivity.n: nat
IHn: nat_pow 1 n = 1
nat_pow 1 n + 0 = 1
  lhs napply nat_add_zero_r.n: nat
IHn: nat_pow 1 n = 1
nat_pow 1 n = 1
  exact IHn.
Defined.

(** Any number to the power of [1] is itself. *)
Definition nat_pow_one_r@{} n : nat_pow n 1 = n
  := nat_mul_one_r _.

(** Exponentiation of natural numbers is distributive over addition on the left. *)
Definition nat_pow_add_r@{} n m k
  : nat_pow n (m + k) = nat_pow n m * nat_pow n k.n, m, k: nat
nat_pow n (m + k) = nat_pow n m * nat_pow n k
Proof.n, m, k: nat
nat_pow n (m + k) = nat_pow n m * nat_pow n k
  induction m as [|m IHm]; simpl.n, k: nat
nat_pow n k = nat_pow n k + 0
n, m, k: nat
IHm: nat_pow n (m + k) = nat_pow n m * nat_pow n k
n * nat_pow n (m + k) = n * nat_pow n m * nat_pow n k
  -n, k: nat
nat_pow n k = nat_pow n k + 0 symmetry.n, k: nat
nat_pow n k + 0 = nat_pow n k
    apply nat_add_zero_r.
  -n, m, k: nat
IHm: nat_pow n (m + k) = nat_pow n m * nat_pow n k
n * nat_pow n (m + k) = n * nat_pow n m * nat_pow n k rhs_V napply nat_mul_assoc.n, m, k: nat
IHm: nat_pow n (m + k) = nat_pow n m * nat_pow n k
n * nat_pow n (m + k) =
n * (nat_pow n m * nat_pow n k)
    exact (ap _ IHm).
Defined.

(** Exponentiation of natural numbers is distributive over multiplication on the right. *)
Definition nat_pow_mul_l@{} n m k
  : nat_pow (n * m) k = nat_pow n k * nat_pow m k.n, m, k: nat
nat_pow (n * m) k = nat_pow n k * nat_pow m k
Proof.n, m, k: nat
nat_pow (n * m) k = nat_pow n k * nat_pow m k
  induction k as [|k IHk]; simpl.n, m: nat
1 = 1
n, m, k: nat
IHk: nat_pow (n * m) k = nat_pow n k * nat_pow m k
n * m * nat_pow (n * m) k =
n * nat_pow n k * (m * nat_pow m k)
  1: reflexivity.n, m, k: nat
IHk: nat_pow (n * m) k = nat_pow n k * nat_pow m k
n * m * nat_pow (n * m) k =
n * nat_pow n k * (m * nat_pow m k)
  lhs_V napply nat_mul_assoc.n, m, k: nat
IHk: nat_pow (n * m) k = nat_pow n k * nat_pow m k
n * (m * nat_pow (n * m) k) =
n * nat_pow n k * (m * nat_pow m k)
  rhs_V napply nat_mul_assoc.n, m, k: nat
IHk: nat_pow (n * m) k = nat_pow n k * nat_pow m k
n * (m * nat_pow (n * m) k) =
n * (nat_pow n k * (m * nat_pow m k))
  napply ap.n, m, k: nat
IHk: nat_pow (n * m) k = nat_pow n k * nat_pow m k
m * nat_pow (n * m) k =
nat_pow n k * (m * nat_pow m k)
  rhs napply nat_mul_comm.n, m, k: nat
IHk: nat_pow (n * m) k = nat_pow n k * nat_pow m k
m * nat_pow (n * m) k = m * nat_pow m k * nat_pow n k
  rhs_V napply nat_mul_assoc.n, m, k: nat
IHk: nat_pow (n * m) k = nat_pow n k * nat_pow m k
m * nat_pow (n * m) k =
m * (nat_pow m k * nat_pow n k)
  napply ap.n, m, k: nat
IHk: nat_pow (n * m) k = nat_pow n k * nat_pow m k
nat_pow (n * m) k = nat_pow m k * nat_pow n k
  rhs napply nat_mul_comm.n, m, k: nat
IHk: nat_pow (n * m) k = nat_pow n k * nat_pow m k
nat_pow (n * m) k = nat_pow n k * nat_pow m k
  exact IHk.
Defined.

(** Exponentiation of natural numbers is distributive over multiplication on the left. *)
Definition nat_pow_mul_r@{} n m k
  : nat_pow n (m * k) = nat_pow (nat_pow n m) k.n, m, k: nat
nat_pow n (m * k) = nat_pow (nat_pow n m) k
Proof.n, m, k: nat
nat_pow n (m * k) = nat_pow (nat_pow n m) k
  induction m as [|m IHm]; simpl.n, k: nat
1 = nat_pow 1 k
n, m, k: nat
IHm: nat_pow n (m * k) = nat_pow (nat_pow n m) k
nat_pow n (k + m * k) = nat_pow (n * nat_pow n m) k
  -n, k: nat
1 = nat_pow 1 k exact (nat_pow_one_l _)^.
  -n, m, k: nat
IHm: nat_pow n (m * k) = nat_pow (nat_pow n m) k
nat_pow n (k + m * k) = nat_pow (n * nat_pow n m) k lhs napply nat_pow_add_r.n, m, k: nat
IHm: nat_pow n (m * k) = nat_pow (nat_pow n m) k
nat_pow n k * nat_pow n (m * k) =
nat_pow (n * nat_pow n m) k
    rhs napply nat_pow_mul_l.n, m, k: nat
IHm: nat_pow n (m * k) = nat_pow (nat_pow n m) k
nat_pow n k * nat_pow n (m * k) =
nat_pow n k * nat_pow (nat_pow n m) k
    napply ap.n, m, k: nat
IHm: nat_pow n (m * k) = nat_pow (nat_pow n m) k
nat_pow n (m * k) = nat_pow (nat_pow n m) k
    exact IHm.
Defined.

(** *** Monotonicity of powers *)

Definition nat_pow_l_monotone {n m} k
  : n <= m -> nat_pow k.+1 n <= nat_pow k.+1 m.n, m, k: nat
n <= m -> nat_pow k.+1 n <= nat_pow k.+1 m
Proof.n, m, k: nat
n <= m -> nat_pow k.+1 n <= nat_pow k.+1 m
  intros H; induction H; exact _.
Defined.

Definition nat_pow_r_monotone {n m} k
  : n <= m -> nat_pow n k <= nat_pow m k.n, m, k: nat
n <= m -> nat_pow n k <= nat_pow m k
Proof.n, m, k: nat
n <= m -> nat_pow n k <= nat_pow m k
  intros H; induction k; exact _.
Defined.

(** ** Strong induction *)

(** Sometimes using [nat_ind] is not sufficient to prove a statement as it may be difficult to prove [P n -> P n.+1]. We can strengthen the induction hypothesis by assuming that [P m] holds for all [m] less than [n]. This is known as strong induction. *)
Definition nat_ind_strong@{u} (P : nat -> Type@{u})
  (IH_strong : forall n, (forall m, m < n -> P m) -> P n)
  : forall n, P n.P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
forall n : nat, P n
Proof.P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
forall n : nat, P n
  intros n.P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
P n
  apply IH_strong.P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
forall m : nat, m < n -> P m
  simple_induction n n IHn; intros m H.P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
m: nat
H: m < 0
P m
P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
m: nat
H: m < n.+1
P m
  1: contradiction (not_lt_zero_r m).P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
m: nat
H: m < n.+1
P m
  apply leq_pred' in H.P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
m: nat
H: m <= n
P m
  apply equiv_leq_lt_or_eq in H.P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
m: nat
H: ((m < n) + (m = n))%type
P m
  destruct H as [H|p].P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
m: nat
H: m < n
P m
P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
m: nat
p: m = n
P m
  -P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
m: nat
H: m < n
P m by apply IHn.
  -P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
n: nat
IHn: forall m : nat, m < n -> P m
m: nat
p: m = n
P m destruct p.P: nat -> Type
IH_strong: forall n : nat,
(forall m : nat, m < n -> P m) -> P n
m: nat
IHn: forall m0 : nat, m0 < m -> P m0
P m
    by apply IH_strong.
Defined.

(** ** An induction principle for two variables with a constraint. *)
Definition nat_double_ind_leq@{u} (P : nat -> nat -> Type@{u})
  (Hn0 : forall n, P n 0)
  (Hnn : forall n, P n.+1 n.+1)
  (IH : forall n m, m < n -> (forall m', m' <= n -> P n m') -> P n.+1 m.+1)
  : forall n m, m <= n -> P n m.P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
forall n m : nat, m <= n -> P n m
Proof.P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
forall n m : nat, m <= n -> P n m
  intro n; simple_induction n n IHn; intros m H.P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
m: nat
H: m <= 0
P 0 m
P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
n: nat
IHn: forall m : nat, m <= n -> P n m
m: nat
H: m <= n.+1
P n.+1 m
  -P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
m: nat
H: m <= 0
P 0 m destruct (path_zero_leq_zero_r m H)^; clear H.P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
P 0 0
    apply Hn0.
  -P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
n: nat
IHn: forall m : nat, m <= n -> P n m
m: nat
H: m <= n.+1
P n.+1 m destruct m.P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
n: nat
IHn: forall m : nat, m <= n -> P n m
H: 0 <= n.+1
P n.+1 0
P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
n: nat
IHn: forall m : nat, m <= n -> P n m
m: nat
H: m.+1 <= n.+1
P n.+1 m.+1
    +P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
n: nat
IHn: forall m : nat, m <= n -> P n m
H: 0 <= n.+1
P n.+1 0 apply Hn0.
    +P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
n: nat
IHn: forall m : nat, m <= n -> P n m
m: nat
H: m.+1 <= n.+1
P n.+1 m.+1 apply equiv_leq_lt_or_eq in H.P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
n: nat
IHn: forall m : nat, m <= n -> P n m
m: nat
H: ((m.+1 < n.+1) + (m.+1 = n.+1))%type
P n.+1 m.+1
      destruct H as [H | []].P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
n: nat
IHn: forall m : nat, m <= n -> P n m
m: nat
H: m.+1 < n.+1
P n.+1 m.+1
P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
n: nat
IHn: forall m : nat, m <= n -> P n m
m: nat
P m.+1 m.+1
      2: apply Hnn.P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
n: nat
IHn: forall m : nat, m <= n -> P n m
m: nat
H: m.+1 < n.+1
P n.+1 m.+1
      rapply IH.P: nat -> nat -> Type
Hn0: forall n : nat, P n 0
Hnn: forall n : nat, P n.+1 n.+1
IH: forall n m : nat,
m < n ->
(forall m' : nat, m' <= n -> P n m') ->
P n.+1 m.+1
n: nat
IHn: forall m : nat, m <= n -> P n m
m: nat
H: m.+1 < n.+1
forall m' : nat, m' <= n -> P n m'
      exact IHn.
Defined.