Division.v

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

Local Set Universe Minimization ToSet.
Local Open Scope nat_scope.

(** * Division of natural numbers *)

(** ** Divisibility *)

(** We define divisibility as a relation between natural numbers. *)
Class NatDivides (n m : nat) : Type0 := nat_divides : {k : nat & k * n = m}.

Notation "( n | m )" := (NatDivides n m) : nat_scope.

(** Any number divides [0]. *)
Instance nat_divides_zero_r n : (n | 0)
  := (0; idpath).

(** [1] divides any number. *)
Instance nat_divides_one_l n : (1 | n)
  := (n; nat_mul_one_r _).

(** Any number divides itself. Divisibility is a reflexive relation. *)
Instance nat_divides_refl n : (n | n)
  := (1; nat_mul_one_l _).

Instance reflexive_nat_divides : Reflexive NatDivides := nat_divides_refl.

(** Divisibility is transitive. *)
Definition nat_divides_trans {n m l} : (n | m) -> (m | l) -> (n | l).n, m, l: nat
(n | m) -> (m | l) -> (n | l)
Proof.n, m, l: nat
(n | m) -> (m | l) -> (n | l)
  intros [x p] [y q].n, m, l, x: nat
p: x * n = m
y: nat
q: y * m = l
(n | l)
  exists (y * x).n, m, l, x: nat
p: x * n = m
y: nat
q: y * m = l
y * x * n = l
  lhs_V napply nat_mul_assoc.n, m, l, x: nat
p: x * n = m
y: nat
q: y * m = l
y * (x * n) = l
  lhs napply (ap _ p).n, m, l, x: nat
p: x * n = m
y: nat
q: y * m = l
y * m = l
  exact q.
Defined.
Hint Immediate nat_divides_trans : typeclass_instances.

Instance transitive_nat_divides : Transitive NatDivides := @nat_divides_trans.

(** A left factor divides a product. *)
Instance nat_divides_mul_l' n m : (n | n * m)
  := (m; nat_mul_comm _ _).

(** A right factor divides a product. *)
Instance nat_divides_mul_r' n m : (m | n * m)
  := (n; idpath).

(** Divisibility of the product is implied by divisibility of the left factor. *)
Instance nat_divides_mul_l {n m} l : (n | m) -> (n | m * l)
  := fun H => nat_divides_trans _ _.

(** Divisibility of the product is implied by divisibility of the right factor. *)
Instance nat_divides_mul_r {n m} l : (n | m) -> (n | l * m)
  := fun H => nat_divides_trans _ _.

(** Multiplication is monotone with respect to divisibility. *)
Instance nat_divides_mul_monotone n m l p
  : (n | m) -> (l | p) -> (n * l | m * p).n, m, l, p: nat
(n | m) -> (l | p) -> (n * l | m * p)
Proof.n, m, l, p: nat
(n | m) -> (l | p) -> (n * l | m * p)
  intros [x r] [y q].n, m, l, p, x: nat
r: x * n = m
y: nat
q: y * l = p
(n * l | m * p)
  exists (x * y).n, m, l, p, x: nat
r: x * n = m
y: nat
q: y * l = p
x * y * (n * l) = m * p
  destruct r, q.n, l, x, y: nat
x * y * (n * l) = x * n * (y * l)
  lhs napply nat_mul_assoc.n, l, x, y: nat
x * y * n * l = x * n * (y * l)
  rhs napply nat_mul_assoc.n, l, x, y: nat
x * y * n * l = x * n * y * l
  napply (ap (fun x => nat_mul x _)).n, l, x, y: nat
x * y * n = x * n * y
  lhs_V napply nat_mul_assoc.n, l, x, y: nat
x * (y * n) = x * n * y
  rhs_V napply nat_mul_assoc.n, l, x, y: nat
x * (y * n) = x * (n * y)
  napply ap.n, l, x, y: nat
y * n = n * y
  apply nat_mul_comm.
Defined.

(** Divisibility of the sum is implied by divisibility of the summands. *)
Instance nat_divides_add n m l : (n | m) -> (n | l) -> (n | m + l).n, m, l: nat
(n | m) -> (n | l) -> (n | m + l)
Proof.n, m, l: nat
(n | m) -> (n | l) -> (n | m + l)
  intros [x p] [y q].n, m, l, x: nat
p: x * n = m
y: nat
q: y * n = l
(n | m + l)
  exists (x + y).n, m, l, x: nat
p: x * n = m
y: nat
q: y * n = l
(x + y) * n = m + l
  destruct p, q.n, x, y: nat
(x + y) * n = x * n + y * n
  napply nat_dist_r.
Defined.

(** If [n] divides a sum and the left summand, then [n] divides the right summand. *)
Definition nat_divides_add_r n m l : (n | m) -> (n | m + l) -> (n | l).n, m, l: nat
(n | m) -> (n | m + l) -> (n | l)
Proof.n, m, l: nat
(n | m) -> (n | m + l) -> (n | l)
  intros [x p] [y q].n, m, l, x: nat
p: x * n = m
y: nat
q: y * n = m + l
(n | l)
  exists (y - x).n, m, l, x: nat
p: x * n = m
y: nat
q: y * n = m + l
(y - x) * n = l
  lhs napply nat_dist_sub_r.n, m, l, x: nat
p: x * n = m
y: nat
q: y * n = m + l
y * n - x * n = l
  apply nat_moveR_nV.n, m, l, x: nat
p: x * n = m
y: nat
q: y * n = m + l
y * n = l + x * n
  lhs exact q.n, m, l, x: nat
p: x * n = m
y: nat
q: y * n = m + l
m + l = l + x * n
  lhs napply nat_add_comm.n, m, l, x: nat
p: x * n = m
y: nat
q: y * n = m + l
l + m = l + x * n
  exact (ap _ p^).
Defined.

(** If [n] divides a sum and the right summand, then [n] divides the left summand. *)
Definition nat_divides_add_l n m l : (n | l) -> (n | m + l) -> (n | m).n, m, l: nat
(n | l) -> (n | m + l) -> (n | m)
Proof.n, m, l: nat
(n | l) -> (n | m + l) -> (n | m)
  rewrite nat_add_comm; apply nat_divides_add_r.
Defined.

(** Divisibility of the difference is implied by divisibility of the minuend and subtrahend. *)
Instance nat_divides_sub n m l : (n | m) -> (n | l) -> (n | m - l).n, m, l: nat
(n | m) -> (n | l) -> (n | m - l)
Proof.n, m, l: nat
(n | m) -> (n | l) -> (n | m - l)
  intros [x p] [y q].n, m, l, x: nat
p: x * n = m
y: nat
q: y * n = l
(n | m - l)
  exists (x - y).n, m, l, x: nat
p: x * n = m
y: nat
q: y * n = l
(x - y) * n = m - l
  destruct p, q.n, x, y: nat
(x - y) * n = x * n - y * n
  napply nat_dist_sub_r.
Defined.

(** The divisor is greater than zero when the number being divided is greater than zero. *)
Definition gt_zero_divides n m (d : (n | m)) (gt0 : 0 < m)
  : 0 < n.n, m: nat
d: (n | m)
gt0: 0 < m
0 < n
Proof.n, m: nat
d: (n | m)
gt0: 0 < m
0 < n
  destruct d as [d H].n, m, d: nat
H: d * n = m
gt0: 0 < m
0 < n
  destruct H.n, d: nat
gt0: 0 < d * n
0 < n
  destruct (nat_zero_or_gt_zero n) as [z | s].n, d: nat
gt0: 0 < d * n
z: 0 = n
0 < n
n, d: nat
gt0: 0 < d * n
s: 0 < n
0 < n
  2: exact s.n, d: nat
gt0: 0 < d * n
z: 0 = n
0 < n
  (* The remaining case is impossible. *)
  destruct z; cbn in gt0.d: nat
gt0: 0 < d * 0
0 < 0
  rewrite nat_mul_zero_r in gt0.d: nat
gt0: 0 < 0
0 < 0
  exact gt0.
Defined.

(** Divisibility implies that the divisor is less than or equal to the dividend. *)
Definition leq_divides n m : 0 < m -> (n | m) -> n <= m.n, m: nat
0 < m -> (n | m) -> n <= m
Proof.n, m: nat
0 < m -> (n | m) -> n <= m
  intros H1 [x p].n, m: nat
H1: 0 < m
x: nat
p: x * n = m
n <= m
  destruct p, x.n: nat
H1: 0 < 0 * n
n <= 0 * n
n, x: nat
H1: 0 < x.+1 * n
n <= x.+1 * n
  1: contradiction (not_lt_zero_r _ H1).n, x: nat
H1: 0 < x.+1 * n
n <= x.+1 * n
  rapply (leq_mul_l _ _ 0).
Defined.

(** The divisor is strictly less than the dividend when the other factor is greater than one. *)
Definition lt_divides n m (d : (n | m)) (gt0 : 0 < m) (gt1 : 1 < d.1)
  : n < m.n, m: nat
d: (n | m)
gt0: 0 < m
gt1: 1 < d.1
n < m
Proof.n, m: nat
d: (n | m)
gt0: 0 < m
gt1: 1 < d.1
n < m
  rewrite <- d.2.n, m: nat
d: (n | m)
gt0: 0 < m
gt1: 1 < d.1
n < d.1 * n
  snapply (lt_leq_lt_trans (m:=1*n)).n, m: nat
d: (n | m)
gt0: 0 < m
gt1: 1 < d.1
n <= 1 * n
n, m: nat
d: (n | m)
gt0: 0 < m
gt1: 1 < d.1
1 * n < d.1 * n
  1: rapply (leq_mul_l _ _ 0).n, m: nat
d: (n | m)
gt0: 0 < m
gt1: 1 < d.1
1 * n < d.1 * n
  srapply (nat_mul_r_strictly_monotone (l:=0)).n, m: nat
d: (n | m)
gt0: 0 < m
gt1: 1 < d.1
0 < n
  rapply (gt_zero_divides n m).
Defined.

(** Divisibility is antisymmetric *)
Definition nat_divides_antisym 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 H1 H2.n, m: nat
H1: (n | m)
H2: (m | n)
n = m
  destruct m; only 1: exact (H2.2^ @ nat_mul_zero_r _).n, m: nat
H1: (n | m.+1)
H2: (m.+1 | n)
n = m.+1
  destruct n; only 1: exact ((nat_mul_zero_r _)^ @ H1.2).n, m: nat
H1: (n.+1 | m.+1)
H2: (m.+1 | n.+1)
n.+1 = m.+1
  snapply leq_antisym; napply leq_divides; exact _.
Defined.

Instance antisymmetric_divides : AntiSymmetric NatDivides
  := nat_divides_antisym.

(** If [n] divides [m], then the other factor also divides [m]. *)
Instance divides_divisor n m (H : (n | m)) : (H.1 | m).n, m: nat
H: (n | m)
(H.1 | m)
Proof.n, m: nat
H: (n | m)
(H.1 | m)
  exists n.n, m: nat
H: (n | m)
n * H.1 = m
  lhs napply nat_mul_comm.n, m: nat
H: (n | m)
H.1 * n = m
  exact H.2.
Defined.

(** ** Properties of division *)

Local Definition nat_div_mod_unique_helper b q1 q2 r1 r2
  : r1 < b -> r2 < b -> q1 < q2 -> b * q1 + r1 <> b * q2 + r2.b, q1, q2, r1, r2: nat
r1 < b ->
r2 < b -> q1 < q2 -> b * q1 + r1 <> b * q2 + r2
Proof.b, q1, q2, r1, r2: nat
r1 < b ->
r2 < b -> q1 < q2 -> b * q1 + r1 <> b * q2 + r2
  intros H1 H2 H3 p.b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: b * q1 + r1 = b * q2 + r2
Empty
  rewrite 2 (nat_add_comm (b * _)) in p.b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: r1 + b * q1 = r2 + b * q2
Empty
  apply nat_moveL_nV in p.b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: r1 = r2 + b * q2 - b * q1
Empty
  rewrite nat_sub_l_add_r in p; only 2: rapply nat_mul_l_monotone.b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: r1 = r2 + (b * q2 - b * q1)
Empty
  rewrite <- nat_dist_sub_l in p.b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: r1 = r2 + b * (q2 - q1)
Empty
  rewrite nat_add_comm in p.b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: r1 = b * (q2 - q1) + r2
Empty
  apply nat_moveR_nV in p.b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: r1 - r2 = b * (q2 - q1)
Empty
  napply (snd (@leq_iff_not_gt b (r1 - r2))).b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: r1 - r2 = b * (q2 - q1)
b <= r1 - r2
b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: r1 - r2 = b * (q2 - q1)
b > r1 - r2
  2: exact (lt_leq_lt_trans _ H1).b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: r1 - r2 = b * (q2 - q1)
b <= r1 - r2
  rewrite p.b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: r1 - r2 = b * (q2 - q1)
b <= b * (q2 - q1)
  snapply (leq_mul_r _ _ 0).b, q1, q2, r1, r2: nat
H1: r1 < b
H2: r2 < b
H3: q1 < q2
p: r1 - r2 = b * (q2 - q1)
0 < q2 - q1
  by apply equiv_lt_lt_sub.
Defined.

(** Quotients and remainders are uniquely determined. *)
Definition nat_div_mod_unique d q1 q2 r1 r2
  : r1 < d -> r2 < d -> d * q1 + r1 = d * q2 + r2
    -> q1 = q2 /\ r1 = r2.d, q1, q2, r1, r2: nat
r1 < d ->
r2 < d ->
d * q1 + r1 = d * q2 + r2 -> (q1 = q2) * (r1 = r2)
Proof.d, q1, q2, r1, r2: nat
r1 < d ->
r2 < d ->
d * q1 + r1 = d * q2 + r2 -> (q1 = q2) * (r1 = r2)
  intros H1 H2 p.d, q1, q2, r1, r2: nat
H1: r1 < d
H2: r2 < d
p: d * q1 + r1 = d * q2 + r2
((q1 = q2) * (r1 = r2))%type
  destruct (nat_trichotomy q1 q2) as [[q | q] | q].d, q1, q2, r1, r2: nat
H1: r1 < d
H2: r2 < d
p: d * q1 + r1 = d * q2 + r2
q: q1 < q2
((q1 = q2) * (r1 = r2))%type
d, q1, q2, r1, r2: nat
H1: r1 < d
H2: r2 < d
p: d * q1 + r1 = d * q2 + r2
q: q1 = q2
((q1 = q2) * (r1 = r2))%type
d, q1, q2, r1, r2: nat
H1: r1 < d
H2: r2 < d
p: d * q1 + r1 = d * q2 + r2
q: q1 > q2
((q1 = q2) * (r1 = r2))%type
  -d, q1, q2, r1, r2: nat
H1: r1 < d
H2: r2 < d
p: d * q1 + r1 = d * q2 + r2
q: q1 < q2
((q1 = q2) * (r1 = r2))%type contradiction (nat_div_mod_unique_helper d q1 q2 r1 r2).
  -d, q1, q2, r1, r2: nat
H1: r1 < d
H2: r2 < d
p: d * q1 + r1 = d * q2 + r2
q: q1 = q2
((q1 = q2) * (r1 = r2))%type split; trivial.d, q1, q2, r1, r2: nat
H1: r1 < d
H2: r2 < d
p: d * q1 + r1 = d * q2 + r2
q: q1 = q2
r1 = r2
    destruct q.d, q1, r1, r2: nat
H1: r1 < d
H2: r2 < d
p: d * q1 + r1 = d * q1 + r2
r1 = r2
    by apply isinj_nat_add_l in p.
  -d, q1, q2, r1, r2: nat
H1: r1 < d
H2: r2 < d
p: d * q1 + r1 = d * q2 + r2
q: q1 > q2
((q1 = q2) * (r1 = r2))%type by contradiction (nat_div_mod_unique_helper d q2 q1 r2 r1).
Defined.

(** Divisibility by a positive natural number is a hprop. *)
Instance ishprop_nat_divides n m : 0 < n -> IsHProp (n | m).n, m: nat
0 < n -> IsHProp (n | m)
Proof.n, m: nat
0 < n -> IsHProp (n | m)
  intros H.n, m: nat
H: 0 < n
IsHProp (n | m)
  apply hprop_allpath.n, m: nat
H: 0 < n
forall x y : (n | m), x = y
  intros [x p] [y q].n, m: nat
H: 0 < n
x: nat
p: x * n = m
y: nat
q: y * n = m
(x; p) = (y; q)
  rapply path_sigma_hprop.n, m: nat
H: 0 < n
x: nat
p: x * n = m
y: nat
q: y * n = m
(x; p).1 = (y; q).1
  destruct H as [|n]; simpl.m, x: nat
p: x * 1 = m
y: nat
q: y * 1 = m
x = y
m, n: nat
H: 1 <= n
x: nat
p: x * n.+1 = m
y: nat
q: y * n.+1 = m
x = y
  1: exact ((nat_mul_one_r _)^ @ p @ q^ @ nat_mul_one_r _).m, n: nat
H: 1 <= n
x: nat
p: x * n.+1 = m
y: nat
q: y * n.+1 = m
x = y
  refine (fst (nat_div_mod_unique n.+1 x y 0 0 _ _ _)).m, n: nat
H: 1 <= n
x: nat
p: x * n.+1 = m
y: nat
q: y * n.+1 = m
n.+1 * x + 0 = n.+1 * y + 0
  lhs napply nat_add_zero_r.m, n: nat
H: 1 <= n
x: nat
p: x * n.+1 = m
y: nat
q: y * n.+1 = m
n.+1 * x = n.+1 * y + 0
  rhs napply nat_add_zero_r.m, n: nat
H: 1 <= n
x: nat
p: x * n.+1 = m
y: nat
q: y * n.+1 = m
n.+1 * x = n.+1 * y
  rewrite 2 (nat_mul_comm n.+1).m, n: nat
H: 1 <= n
x: nat
p: x * n.+1 = m
y: nat
q: y * n.+1 = m
x * n.+1 = y * n.+1
  exact (p @ q^).
Defined.

(** This specifies the behaviour of [nat_div_mod_helper] when [u <= y]. *)
Definition nat_div_mod_helper_spec x y q u (H : u <= y)
  : let (q', u') := nat_div_mod x y q u in
     x + y.+1 * q + (y - u) = y.+1 * q' + (y - u') /\ u' <= y.x, y, q, u: nat
H: u <= y
let q' := fst (nat_div_mod x y q u) in
let u' := snd (nat_div_mod x y q u) in
(((x + y.+1 * q + (y - u))%nat =
  (y.+1 * q' + (y - u'))%nat) * (u' <= y))%type
Proof.x, y, q, u: nat
H: u <= y
let q' := fst (nat_div_mod x y q u) in
let u' := snd (nat_div_mod x y q u) in
(((x + y.+1 * q + (y - u))%nat =
  (y.+1 * q' + (y - u'))%nat) * (u' <= y))%type
  intros d r.x, y, q, u: nat
H: u <= y
d:= fst (nat_div_mod x y q u): nat
r:= snd (nat_div_mod x y q u): nat
(((x + y.+1 * q + (y - u))%nat =
  (y.+1 * d + (y - r))%nat) * (r <= y))%type
  induction x as [|x IHx] in y, q, u, H, d, r |- *; only 1: by split.x, y, q, u: nat
H: u <= y
d:= fst (nat_div_mod x.+1 y q u): nat
r:= snd (nat_div_mod x.+1 y q u): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
(((x.+1 + y.+1 * q + (y - u))%nat =
  (y.+1 * d + (y - r))%nat) * (r <= y))%type
  destruct u as [|u].x, y, q: nat
H: 0 <= y
d:= fst (nat_div_mod x.+1 y q 0): nat
r:= snd (nat_div_mod x.+1 y q 0): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
(((x.+1 + y.+1 * q + (y - 0))%nat =
  (y.+1 * d + (y - r))%nat) * (r <= y))%type
x, y, q, u: nat
H: u.+1 <= y
d:= fst (nat_div_mod x.+1 y q u.+1): nat
r:= snd (nat_div_mod x.+1 y q u.+1): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
(((x.+1 + y.+1 * q + (y - u.+1))%nat =
  (y.+1 * d + (y - r))%nat) * (r <= y))%type
  -x, y, q: nat
H: 0 <= y
d:= fst (nat_div_mod x.+1 y q 0): nat
r:= snd (nat_div_mod x.+1 y q 0): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
(((x.+1 + y.+1 * q + (y - 0))%nat =
  (y.+1 * d + (y - r))%nat) * (r <= y))%type destruct (IHx y q.+1 y _) as [p H'].x, y, q: nat
H: 0 <= y
d:= fst (nat_div_mod x.+1 y q 0): nat
r:= snd (nat_div_mod x.+1 y q 0): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
p: x + y.+1 * q.+1 + (y - y) =
y.+1 * fst (nat_div_mod x y q.+1 y) +
(y - snd (nat_div_mod x y q.+1 y))
H': snd (nat_div_mod x y q.+1 y) <= y
(((x.+1 + y.+1 * q + (y - 0))%nat =
  (y.+1 * d + (y - r))%nat) * (r <= y))%type
    split; trivial.x, y, q: nat
H: 0 <= y
d:= fst (nat_div_mod x.+1 y q 0): nat
r:= snd (nat_div_mod x.+1 y q 0): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
p: x + y.+1 * q.+1 + (y - y) =
y.+1 * fst (nat_div_mod x y q.+1 y) +
(y - snd (nat_div_mod x y q.+1 y))
H': snd (nat_div_mod x y q.+1 y) <= y
x.+1 + y.+1 * q + (y - 0) = y.+1 * d + (y - r)
    rewrite <- p, nat_sub_zero_r, nat_sub_cancel, nat_add_zero_r.x, y, q: nat
H: 0 <= y
d:= fst (nat_div_mod x.+1 y q 0): nat
r:= snd (nat_div_mod x.+1 y q 0): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
p: x + y.+1 * q.+1 + (y - y) =
y.+1 * fst (nat_div_mod x y q.+1 y) +
(y - snd (nat_div_mod x y q.+1 y))
H': snd (nat_div_mod x y q.+1 y) <= y
x.+1 + y.+1 * q + y = x + y.+1 * q.+1
    simpl.x, y, q: nat
H: 0 <= y
d:= fst (nat_div_mod x.+1 y q 0): nat
r:= snd (nat_div_mod x.+1 y q 0): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
p: x + y.+1 * q.+1 + (y - y) =
y.+1 * fst (nat_div_mod x y q.+1 y) +
(y - snd (nat_div_mod x y q.+1 y))
H': snd (nat_div_mod x y q.+1 y) <= y
(x + (q + y * q) + y).+1 = x + (q + y * q.+1).+1
    by rewrite nat_add_succ_r, <- 2 nat_add_assoc, nat_mul_succ_r.
  -x, y, q, u: nat
H: u.+1 <= y
d:= fst (nat_div_mod x.+1 y q u.+1): nat
r:= snd (nat_div_mod x.+1 y q u.+1): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
(((x.+1 + y.+1 * q + (y - u.+1))%nat =
  (y.+1 * d + (y - r))%nat) * (r <= y))%type destruct (IHx y q u _) as [p H'].x, y, q, u: nat
H: u.+1 <= y
d:= fst (nat_div_mod x.+1 y q u.+1): nat
r:= snd (nat_div_mod x.+1 y q u.+1): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
p: x + y.+1 * q + (y - u) =
y.+1 * fst (nat_div_mod x y q u) +
(y - snd (nat_div_mod x y q u))
H': snd (nat_div_mod x y q u) <= y
(((x.+1 + y.+1 * q + (y - u.+1))%nat =
  (y.+1 * d + (y - r))%nat) * (r <= y))%type
    split; trivial.x, y, q, u: nat
H: u.+1 <= y
d:= fst (nat_div_mod x.+1 y q u.+1): nat
r:= snd (nat_div_mod x.+1 y q u.+1): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
p: x + y.+1 * q + (y - u) =
y.+1 * fst (nat_div_mod x y q u) +
(y - snd (nat_div_mod x y q u))
H': snd (nat_div_mod x y q u) <= y
x.+1 + y.+1 * q + (y - u.+1) = y.+1 * d + (y - r)
    rewrite <- p, 2 nat_add_succ_l, <- nat_add_succ_r.x, y, q, u: nat
H: u.+1 <= y
d:= fst (nat_div_mod x.+1 y q u.+1): nat
r:= snd (nat_div_mod x.+1 y q u.+1): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
p: x + y.+1 * q + (y - u) =
y.+1 * fst (nat_div_mod x y q u) +
(y - snd (nat_div_mod x y q u))
H': snd (nat_div_mod x y q u) <= y
x + y.+1 * q + (y - u.+1).+1 = x + y.+1 * q + (y - u)
    snapply ap.x, y, q, u: nat
H: u.+1 <= y
d:= fst (nat_div_mod x.+1 y q u.+1): nat
r:= snd (nat_div_mod x.+1 y q u.+1): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
p: x + y.+1 * q + (y - u) =
y.+1 * fst (nat_div_mod x y q u) +
(y - snd (nat_div_mod x y q u))
H': snd (nat_div_mod x y q u) <= y
(y - u.+1).+1 = y - u
    rewrite nat_sub_succ_r.x, y, q, u: nat
H: u.+1 <= y
d:= fst (nat_div_mod x.+1 y q u.+1): nat
r:= snd (nat_div_mod x.+1 y q u.+1): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
p: x + y.+1 * q + (y - u) =
y.+1 * fst (nat_div_mod x y q u) +
(y - snd (nat_div_mod x y q u))
H': snd (nat_div_mod x y q u) <= y
(nat_pred (y - u)).+1 = y - u
    apply nat_succ_pred.x, y, q, u: nat
H: u.+1 <= y
d:= fst (nat_div_mod x.+1 y q u.+1): nat
r:= snd (nat_div_mod x.+1 y q u.+1): nat
IHx: forall y q u : nat,
u <= y ->
let d := fst (nat_div_mod x y q u) in
let r := snd (nat_div_mod x y q u) in
(x + y.+1 * q + (y - u) = y.+1 * d + (y - r)) * (r <= y)
p: x + y.+1 * q + (y - u) =
y.+1 * fst (nat_div_mod x y q u) +
(y - snd (nat_div_mod x y q u))
H': snd (nat_div_mod x y q u) <= y
0 < y - u
    rapply lt_moveL_nV.
Defined.

(** Division and modulo can be put in quotient-remainder form. *)
Definition nat_div_mod_spec x y : x = y * (x / y) + x mod y.x, y: nat
x = y * (x / y) + x mod y
Proof.x, y: nat
x = y * (x / y) + x mod y
  destruct y as [|y]; only 1: reflexivity.x, y: nat
x = y.+1 * (x / y.+1) + x mod y.+1
  pose proof (p := fst (nat_div_mod_helper_spec x y 0 y _)).x, y: nat
p: x + y.+1 * 0 + (y - y) =
y.+1 * fst (nat_div_mod x y 0 y) +
(y - snd (nat_div_mod x y 0 y))
x = y.+1 * (x / y.+1) + x mod y.+1
  by rewrite nat_mul_zero_r, nat_sub_cancel, 2 nat_add_zero_r in p.
Defined.

Definition nat_div_mod_spec' x y : x - y * (x / y) = x mod y.x, y: nat
x - y * (x / y) = x mod y
Proof.x, y: nat
x - y * (x / y) = x mod y
  apply nat_moveR_nV.x, y: nat
x = x mod y + y * (x / y)
  rhs napply nat_add_comm.x, y: nat
x = y * (x / y) + x mod y
  apply nat_div_mod_spec.
Defined.

Definition nat_div_mod_spec'' x y : x - x mod y = y * (x / y).x, y: nat
x - x mod y = y * (x / y)
Proof.x, y: nat
x - x mod y = y * (x / y)
  apply nat_moveR_nV.x, y: nat
x = y * (x / y) + x mod y
  apply nat_div_mod_spec.
Defined.

Definition nat_mod_lt_r' n m r : r < m -> n mod m < m.n, m, r: nat
r < m -> n mod m < m
Proof.n, m, r: nat
r < m -> n mod m < m
  intros H; destruct H; only 1: exact _.n, r, m: nat
H: r.+1 <= m
n mod m.+1 < m.+1
  rapply (lt_leq_lt_trans (m:=m)).
Defined.
Hint Immediate nat_mod_lt_r' : typeclass_instances.

(** [n] modulo [m] is less than [m]. *)
Instance nat_mod_lt_r n m : 0 < m -> n mod m < m
  := nat_mod_lt_r' n m 0.

(** [n] modulo [m] is less than or equal to [m]. *)
Instance nat_mod_leq_l n m : n mod m <= n.n, m: nat
n mod m <= n
Proof.n, m: nat
n mod m <= n
  rewrite <- nat_div_mod_spec'.n, m: nat
n - m * (n / m) <= n
  rapply leq_moveR_nV.
Defined.

(** Division is unique. *)
Definition nat_div_unique x y q r (H : r < y) (p : y * q + r = x) : x / y = q
  := fst (nat_div_mod_unique y (x / y) q (x mod y) r _ _ (p @ nat_div_mod_spec x y)^).

(** Modulo is unique. *)
Definition nat_mod_unique x y q r (H : r < y) (p : y * q + r = x) : x mod y = r
  := snd (nat_div_mod_unique y (x / y) q (x mod y) r _ _ (p @ nat_div_mod_spec x y)^).

(** [0] divided by any number is [0]. *)
Definition nat_div_zero_l n : 0 / n = 0.n: nat
0 / n = 0
Proof.n: nat
0 / n = 0
  by induction n.
Defined.

(** [n] divided by [0] is [0] by convention. *)
Definition nat_div_zero_r n : n / 0 = 0 := idpath.

(** [n] divided by [1] is [n]. *)
Definition nat_div_one_r n : n / 1 = n.n: nat
n / 1 = n
Proof.n: nat
n / 1 = n
  lhs_V napply nat_mul_one_l.n: nat
1 * (n / 1) = n
  lhs_V napply nat_add_zero_r.n: nat
1 * (n / 1) + 0 = n
  symmetry; apply nat_div_mod_spec.
Defined.

(** [n] divided by [n] is [1]. *)
Definition nat_div_cancel n : 0 < n -> n / n = 1.n: nat
0 < n -> n / n = 1
Proof.n: nat
0 < n -> n / n = 1
  intros [|m _]; trivial.n, m: nat
m.+1 / m.+1 = 1
  napply (nat_div_unique _ _ _ 0); only 1: exact _.n, m: nat
m.+1 * 1 + 0 = m.+1
  lhs napply nat_add_zero_r.n, m: nat
m.+1 * 1 = m.+1
  napply nat_mul_one_r.
Defined.

(** A number divided by a larger number is 0. *)
Definition nat_div_lt n m : n < m -> n / m = 0.n, m: nat
n < m -> n / m = 0
Proof.n, m: nat
n < m -> n / m = 0
  intros H.n, m: nat
H: n < m
n / m = 0
  snapply (nat_div_unique _ _ _ _ H).n, m: nat
H: n < m
m * 0 + n = n
  by rewrite nat_mul_zero_r, nat_add_zero_l.
Defined.

(** [n * m] divided by [n] is [m]. *)
Definition nat_div_mul_cancel_l n m : 0 < n -> (n * m) / n = m.n, m: nat
0 < n -> (n * m) / n = m
Proof.n, m: nat
0 < n -> (n * m) / n = m
  intros H.n, m: nat
H: 0 < n
(n * m) / n = m
  napply (nat_div_unique _ _ _ _ H).n, m: nat
H: 0 < n
n * m + 0 = n * m
  apply nat_add_zero_r.
Defined.

(** [n * m] divided by [n] is [m]. *)
Definition nat_div_mul_cancel_r n m : 0 < m -> (n * m) / m = n.n, m: nat
0 < m -> (n * m) / m = n
Proof.n, m: nat
0 < m -> (n * m) / m = n
  rewrite nat_mul_comm.n, m: nat
0 < m -> (m * n) / m = n
  apply nat_div_mul_cancel_l.
Defined.

(** More generally, [n * m + k] divided by [n] is [m + k / n]. *)
Definition nat_div_mul_add_cancel_l n m k : 0 < n -> (n * m + k) / n = m + k / n.n, m, k: nat
0 < n -> (n * m + k) / n = m + k / n
Proof.n, m, k: nat
0 < n -> (n * m + k) / n = m + k / n
  intros H.n, m, k: nat
H: 0 < n
(n * m + k) / n = m + k / n
  rapply (nat_div_unique _ _ _ (k mod n) _).n, m, k: nat
H: 0 < n
n * (m + k / n) + k mod n = n * m + k
  rewrite nat_dist_l.n, m, k: nat
H: 0 < n
n * m + n * (k / n) + k mod n = n * m + k
  lhs_V napply nat_add_assoc.n, m, k: nat
H: 0 < n
n * m + (n * (k / n) + k mod n) = n * m + k
  f_ap.n, m, k: nat
H: 0 < n
n * (k / n) + k mod n = k
  symmetry; apply nat_div_mod_spec.
Defined.

Definition nat_div_mul_add_cancel_r n m k : 0 < m -> (n * m + k) / m = n + k / m.n, m, k: nat
0 < m -> (n * m + k) / m = n + k / m
Proof.n, m, k: nat
0 < m -> (n * m + k) / m = n + k / m
  rewrite nat_mul_comm.n, m, k: nat
0 < m -> (m * n + k) / m = n + k / m
  apply nat_div_mul_add_cancel_l.
Defined.

(** If [k] is positive, then multiplication on the left is injective; that is, if [k * m = k * n], then [m = n]. *)
Definition isinj_nat_mul_l k : 0 < k -> IsInjective (nat_mul k).k: nat
0 < k -> IsInjective (nat_mul k)
Proof.k: nat
0 < k -> IsInjective (nat_mul k)
  intros kp m n p.k: nat
kp: 0 < k
m, n: nat
p: k * m = k * n
m = n
  lhs_V rapply (nat_div_mul_cancel_l k).k: nat
kp: 0 < k
m, n: nat
p: k * m = k * n
(k * m) / k = n
  rhs_V rapply (nat_div_mul_cancel_l k).k: nat
kp: 0 < k
m, n: nat
p: k * m = k * n
(k * m) / k = (k * n) / k
  exact (ap (fun x => x / k) p).
Defined.

(** If [k] is positive, then multiplication on the right is injective; that is, if [m * k = n * k], then [m = n]. *)
Definition isinj_nat_mul_r k : 0 < k -> IsInjective (fun n => nat_mul n k).k: nat
0 < k -> IsInjective (fun n : nat => n * k)
Proof.k: nat
0 < k -> IsInjective (fun n : nat => n * k)
  intros kp m n p.k: nat
kp: 0 < k
m, n: nat
p: m * k = n * k
m = n
  lhs_V rapply (nat_div_mul_cancel_r _ k).k: nat
kp: 0 < k
m, n: nat
p: m * k = n * k
(m * k) / k = n
  rhs_V rapply (nat_div_mul_cancel_r _ k).k: nat
kp: 0 < k
m, n: nat
p: m * k = n * k
(m * k) / k = (n * k) / k
  exact (ap (fun x => x / k) p).
Defined.

(** When [d] divides one of the summands, division distributes over addition. *)
Definition nat_div_dist n m d
  : (d | n) -> (n + m) / d = n / d + m / d.n, m, d: nat
(d | n) -> (n + m) / d = n / d + m / d
Proof.n, m, d: nat
(d | n) -> (n + m) / d = n / d + m / d
  destruct d.n, m: nat
(0 | n) -> (n + m) / 0 = n / 0 + m / 0
n, m, d: nat
(d.+1 | n) -> (n + m) / d.+1 = n / d.+1 + m / d.+1
  1: reflexivity.n, m, d: nat
(d.+1 | n) -> (n + m) / d.+1 = n / d.+1 + m / d.+1
  intros [x []].n, m, d, x: nat
(x * d.+1 + m) / d.+1 = (x * d.+1) / d.+1 + m / d.+1
  rewrite nat_div_mul_cancel_r.n, m, d, x: nat
(x * d.+1 + m) / d.+1 = x + m / d.+1
n, m, d, x: nat
0 < d.+1 2: exact _.n, m, d, x: nat
(x * d.+1 + m) / d.+1 = x + m / d.+1
  rapply nat_div_mul_add_cancel_r.
Defined.

Definition nat_div_dist' n m d
  : (d | m) -> (n + m) / d = n / d + m / d.n, m, d: nat
(d | m) -> (n + m) / d = n / d + m / d
Proof.n, m, d: nat
(d | m) -> (n + m) / d = n / d + m / d
  intros H.n, m, d: nat
H: (d | m)
(n + m) / d = n / d + m / d
  rewrite (nat_add_comm n m).n, m, d: nat
H: (d | m)
(m + n) / d = n / d + m / d
  rhs_V napply nat_add_comm.n, m, d: nat
H: (d | m)
(m + n) / d = m / d + n / d
  rapply nat_div_dist.
Defined.

(** In general, [n * (m / n)] is less than or equal to [m]. *)
Definition nat_leq_mul_div_l n m
  : n * (m / n) <= m.n, m: nat
n * (m / n) <= m
Proof.n, m: nat
n * (m / n) <= m
  set (tmp := n * (m / n));
    rewrite (nat_div_mod_spec m n);
    unfold tmp; clear tmp.n, m: nat
n * (m / n) <= n * (m / n) + m mod n
  exact _.
Defined.

(** When [n] divides [m], they are equal. *)
Definition nat_mul_div_cancel_r 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
  destruct n.m: nat
(0 | m) -> m / 0 * 0 = m
n, m: nat
(n.+1 | m) -> m / n.+1 * n.+1 = m
  {m: nat
(0 | m) -> m / 0 * 0 = m intros [k []].m, k: nat
(k * 0) / 0 * 0 = k * 0 cbn.m, k: nat
0 = k * 0 symmetry; apply nat_mul_zero_r. }n, m: nat
(n.+1 | m) -> m / n.+1 * n.+1 = m
  intros [k []].n, m, k: nat
(k * n.+1) / n.+1 * n.+1 = k * n.+1
  f_ap.n, m, k: nat
(k * n.+1) / n.+1 = k
  rapply nat_div_mul_cancel_r.
Defined.

Definition nat_mul_div_cancel_l 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
  rewrite nat_mul_comm.n, m: nat
(n | m) -> m / n * n = m
  apply nat_mul_div_cancel_r.
Defined.

(** Division by non-zero [k] is strictly monotone if [k] divides the larger number. *)
Definition nat_div_strictly_monotone_r {n m l} k
  : l < k -> n < m -> (k | m) -> n / k < m / k.n, m, l, k: nat
l < k -> n < m -> (k | m) -> n / k < m / k
Proof.n, m, l, k: nat
l < k -> n < m -> (k | m) -> n / k < m / k
  intros lk nm km.n, m, l, k: nat
lk: l < k
nm: n < m
km: (k | m)
n / k < m / k
  apply gt_iff_not_leq.n, m, l, k: nat
lk: l < k
nm: n < m
km: (k | m)
~ (m / k <= n / k)
  intro mknk.n, m, l, k: nat
lk: l < k
nm: n < m
km: (k | m)
mknk: m / k <= n / k
Empty
  apply (@gt_iff_not_leq m n); only 1: exact nm.n, m, l, k: nat
lk: l < k
nm: n < m
km: (k | m)
mknk: m / k <= n / k
m <= n
  rewrite <- (nat_mul_div_cancel_l k m km).n, m, l, k: nat
lk: l < k
nm: n < m
km: (k | m)
mknk: m / k <= n / k
k * (m / k) <= n
  napply (leq_trans (y:=k * (n / k))).n, m, l, k: nat
lk: l < k
nm: n < m
km: (k | m)
mknk: m / k <= n / k
k * (m / k) <= k * (n / k)
n, m, l, k: nat
lk: l < k
nm: n < m
km: (k | m)
mknk: m / k <= n / k
k * (n / k) <= n
  -n, m, l, k: nat
lk: l < k
nm: n < m
km: (k | m)
mknk: m / k <= n / k
k * (m / k) <= k * (n / k) rapply nat_mul_l_monotone.
  -n, m, l, k: nat
lk: l < k
nm: n < m
km: (k | m)
mknk: m / k <= n / k
k * (n / k) <= n apply nat_leq_mul_div_l.
Defined.

(** [0] modulo [n] is [0]. *)
Definition nat_mod_zero_l n : 0 mod n = 0.n: nat
0 mod n = 0
Proof.n: nat
0 mod n = 0
  induction n; trivial.n: nat
IHn: 0 mod n = 0
0 mod n.+1 = 0
  apply nat_sub_cancel.
Defined.

(** [n] modulo [0] is [n]. *)
Definition nat_mod_zero_r n : n mod 0 = n := idpath.

Definition nat_mod_lt n k : k < n -> k mod n = k.n, k: nat
k < n -> k mod n = k
Proof.n, k: nat
k < n -> k mod n = k
  intros H.n, k: nat
H: k < n
k mod n = k
  lhs_V napply nat_div_mod_spec'.n, k: nat
H: k < n
k - n * (k / n) = k
  rewrite nat_div_lt.n, k: nat
H: k < n
k - n * 0 = k
n, k: nat
H: k < n
k < n
  -n, k: nat
H: k < n
k - n * 0 = k rewrite nat_mul_zero_r.n, k: nat
H: k < n
k - 0 = k
    apply nat_sub_zero_r.
  -n, k: nat
H: k < n
k < n exact H.
Defined.

(** [n] modulo [1] is [0]. *)
Definition nat_mod_one_r n : n mod 1 = 0.n: nat
n mod 1 = 0
Proof.n: nat
n mod 1 = 0
  by induction n.
Defined.

(** If [m] divides [n], then [n mod m = 0]. *)
Definition nat_mod_divides n m : (m | n) -> n mod m = 0.n, m: nat
(m | n) -> n mod m = 0
Proof.n, m: nat
(m | n) -> n mod m = 0
  intros [x p].n, m, x: nat
p: x * m = n
n mod m = 0
  destruct p.m, x: nat
(x * m) mod m = 0
  destruct m.x: nat
(x * 0) mod 0 = 0
m, x: nat
(x * m.+1) mod m.+1 = 0
  {x: nat
(x * 0) mod 0 = 0 simpl.x: nat
x * 0 = 0 apply nat_mul_zero_r. }m, x: nat
(x * m.+1) mod m.+1 = 0
  lhs_V napply nat_div_mod_spec'.m, x: nat
x * m.+1 - m.+1 * ((x * m.+1) / m.+1) = 0
  rewrite nat_div_mul_cancel_r; only 2: exact _.m, x: nat
x * m.+1 - m.+1 * x = 0
  apply nat_moveR_nV, nat_mul_comm.
Defined.

(** [n mod m = 0] iff [m] divides [n]. *)
Definition nat_mod_iff_divides n m : n mod m = 0 <-> (m | n) .n, m: nat
n mod m = 0 <-> (m | n)
Proof.n, m: nat
n mod m = 0 <-> (m | n)
  split.n, m: nat
n mod m = 0 -> (m | n)
n, m: nat
(m | n) -> n mod m = 0
  2: exact (nat_mod_divides _ _).n, m: nat
n mod m = 0 -> (m | n)
  intros p.n, m: nat
p: n mod m = 0
(m | n)
  exists (n / m).n, m: nat
p: n mod m = 0
n / m * m = n
  rewrite nat_mul_comm.n, m: nat
p: n mod m = 0
m * (n / m) = n
  lhs_V napply nat_add_zero_r.n, m: nat
p: n mod m = 0
m * (n / m) + 0 = n
  rewrite <- p.n, m: nat
p: n mod m = 0
m * (n / m) + n mod m = n
  symmetry.n, m: nat
p: n mod m = 0
n = m * (n / m) + n mod m
  napply nat_div_mod_spec.
Defined.

(** Divisibility is therefore decidable. *)
Instance decidable_nat_divides n m : Decidable (n | m).n, m: nat
Decidable (n | m)
Proof.n, m: nat
Decidable (n | m)
  napply decidable_iff.n, m: nat
?Goal <-> (n | m)
n, m: nat
Decidable ?Goal
  1: apply nat_mod_iff_divides.n, m: nat
Decidable (m mod n = 0)
  exact _.
Defined.

(** [n] modulo [n] is [0]. *)
Definition nat_mod_cancel n : n mod n = 0.n: nat
n mod n = 0
Proof.n: nat
n mod n = 0
  destruct n; trivial.n: nat
n.+1 mod n.+1 = 0
  snapply (nat_mod_unique _ _ 1); only 1: exact _.n: nat
n.+1 * 1 + 0 = n.+1
  lhs napply nat_add_zero_r.n: nat
n.+1 * 1 = n.+1
  napply nat_mul_one_r.
Defined.

(** A number can be corrected so that it is divisible by subtracting the modulo. *)
Instance nat_divides_sub_mod n m : (n | m - m mod n).n, m: nat
(n | m - m mod n)
Proof.n, m: nat
(n | m - m mod n)
  rewrite nat_div_mod_spec''.n, m: nat
(n | n * (m / n))
  exact _.
Defined.

(** ** Further Properties of division and modulo *)

(** We can cancel common factors on the left in a division. *)
Definition nat_div_cancel_mul_l n m k
  : 0 < k -> (k * n) / (k * m) = n / m.n, m, k: nat
0 < k -> (k * n) / (k * m) = n / m
Proof.n, m, k: nat
0 < k -> (k * n) / (k * m) = n / m
  intro kp.n, m, k: nat
kp: 0 < k
(k * n) / (k * m) = n / m
  destruct (nat_zero_or_gt_zero m) as [[] | mp].n, m, k: nat
kp: 0 < k
(k * n) / (k * 0) = n / 0
n, m, k: nat
kp: 0 < k
mp: 0 < m
(k * n) / (k * m) = n / m
  1: by rewrite nat_mul_zero_r.n, m, k: nat
kp: 0 < k
mp: 0 < m
(k * n) / (k * m) = n / m
  napply (nat_div_unique _ _ _ (k * (n mod m))).n, m, k: nat
kp: 0 < k
mp: 0 < m
k * (n mod m) < k * m
n, m, k: nat
kp: 0 < k
mp: 0 < m
k * m * (n / m) + k * (n mod m) = k * n
  1: rapply nat_mul_l_strictly_monotone.n, m, k: nat
kp: 0 < k
mp: 0 < m
k * m * (n / m) + k * (n mod m) = k * n
  rewrite <- nat_mul_assoc.n, m, k: nat
kp: 0 < k
mp: 0 < m
k * (m * (n / m)) + k * (n mod m) = k * n
  rewrite <- nat_dist_l.n, m, k: nat
kp: 0 < k
mp: 0 < m
k * (m * (n / m) + n mod m) = k * n
  apply ap.n, m, k: nat
kp: 0 < k
mp: 0 < m
m * (n / m) + n mod m = n
  symmetry; apply nat_div_mod_spec.
Defined.

(** We can cancel common factors on the right in a division. *)
Definition nat_div_cancel_mul_r n m k
  : 0 < k -> (n * k) / (m * k) = n / m.n, m, k: nat
0 < k -> (n * k) / (m * k) = n / m
Proof.n, m, k: nat
0 < k -> (n * k) / (m * k) = n / m
  rewrite 2 (nat_mul_comm _ k).n, m, k: nat
0 < k -> (k * n) / (k * m) = n / m
  napply nat_div_cancel_mul_l.
Defined.

(** We can swap the order of division and multiplication on the left under certain conditions. *)
Definition nat_div_mul_l n m k : (m | n) -> k * (n / m) = (k * n) / m.n, m, k: nat
(m | n) -> k * (n / m) = (k * n) / m
Proof.n, m, k: nat
(m | n) -> k * (n / m) = (k * n) / m
  intros H.n, m, k: nat
H: (m | n)
k * (n / m) = (k * n) / m
  destruct (nat_zero_or_gt_zero m) as [[] | mp].n, m, k: nat
H: (m | n)
k * (n / 0) = (k * n) / 0
n, m, k: nat
H: (m | n)
mp: 0 < m
k * (n / m) = (k * n) / m
  1: snapply nat_mul_zero_r.n, m, k: nat
H: (m | n)
mp: 0 < m
k * (n / m) = (k * n) / m
  rapply (nat_div_unique _ _ _ 0 _ _)^.n, m, k: nat
H: (m | n)
mp: 0 < m
m * (k * (n / m)) + 0 = k * n
  lhs napply nat_add_zero_r.n, m, k: nat
H: (m | n)
mp: 0 < m
m * (k * (n / m)) = k * n
  lhs napply nat_mul_assoc.n, m, k: nat
H: (m | n)
mp: 0 < m
m * k * (n / m) = k * n
  lhs napply (ap (fun x => x * _)).n, m, k: nat
H: (m | n)
mp: 0 < m
m * k = ?Goal
n, m, k: nat
H: (m | n)
mp: 0 < m
?Goal * (n / m) = k * n
  1: napply nat_mul_comm.n, m, k: nat
H: (m | n)
mp: 0 < m
k * m * (n / m) = k * n
  lhs_V napply nat_mul_assoc.n, m, k: nat
H: (m | n)
mp: 0 < m
k * (m * (n / m)) = k * n
  snapply ap.n, m, k: nat
H: (m | n)
mp: 0 < m
m * (n / m) = n
  lhs_V napply nat_add_zero_r.n, m, k: nat
H: (m | n)
mp: 0 < m
m * (n / m) + 0 = n
  rhs napply (nat_div_mod_spec n m).n, m, k: nat
H: (m | n)
mp: 0 < m
m * (n / m) + 0 = m * (n / m) + n mod m
  snapply ap.n, m, k: nat
H: (m | n)
mp: 0 < m
0 = n mod m
  symmetry.n, m, k: nat
H: (m | n)
mp: 0 < m
n mod m = 0
  rapply nat_mod_divides.
Defined.

(** We can swap the order of division and multiplication on the right under certain conditions. *)
Definition nat_div_mul_r n m k : (m | n) -> (n / m) * k = (n * k) / m.n, m, k: nat
(m | n) -> n / m * k = (n * k) / m
Proof.n, m, k: nat
(m | n) -> n / m * k = (n * k) / m
  rewrite 2 (nat_mul_comm _ k).n, m, k: nat
(m | n) -> k * (n / m) = (k * n) / m
  snapply nat_div_mul_l.
Defined.

Definition nat_div_sub_mod n m : n / m = (n - n mod m) / m.n, m: nat
n / m = (n - n mod m) / m
Proof.n, m: nat
n / m = (n - n mod m) / m
  destruct (nat_zero_or_gt_zero m) as [[] | mp].n, m: nat
n / 0 = (n - n mod 0) / 0
n, m: nat
mp: 0 < m
n / m = (n - n mod m) / m
  1: reflexivity.n, m: nat
mp: 0 < m
n / m = (n - n mod m) / m
  symmetry.n, m: nat
mp: 0 < m
(n - n mod m) / m = n / m
  rewrite nat_div_mod_spec''.n, m: nat
mp: 0 < m
(m * (n / m)) / m = n / m
  rapply nat_div_mul_cancel_l.
Defined.

(** Dividing a quotient is the same as dividing by the product of the divisors. *)
Definition nat_div_div_l 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)
  destruct (nat_zero_or_gt_zero k) as [[] | kp].n, m, k: nat
(n / m) / 0 = n / (m * 0)
n, m, k: nat
kp: 0 < k
(n / m) / k = n / (m * k)
  1: by rewrite nat_mul_zero_r.n, m, k: nat
kp: 0 < k
(n / m) / k = n / (m * k)
  destruct (nat_zero_or_gt_zero m) as [[] | mp].n, m, k: nat
kp: 0 < k
(n / 0) / k = n / (0 * k)
n, m, k: nat
kp: 0 < k
mp: 0 < m
(n / m) / k = n / (m * k)
  1: snapply nat_div_zero_l.n, m, k: nat
kp: 0 < k
mp: 0 < m
(n / m) / k = n / (m * k)
  apply nat_div_unique with (r := (n mod (m * k)) / m).n, m, k: nat
kp: 0 < k
mp: 0 < m
(n mod (m * k)) / m < k
n, m, k: nat
kp: 0 < k
mp: 0 < m
k * (n / (m * k)) + (n mod (m * k)) / m = n / m
  {n, m, k: nat
kp: 0 < k
mp: 0 < m
(n mod (m * k)) / m < k apply (lt_lt_leq_trans (m:=(m * k)/m)).n, m, k: nat
kp: 0 < k
mp: 0 < m
(n mod (m * k)) / m < (m * k) / m
n, m, k: nat
kp: 0 < k
mp: 0 < m
(m * k) / m <= k
    -n, m, k: nat
kp: 0 < k
mp: 0 < m
(n mod (m * k)) / m < (m * k) / m rapply nat_div_strictly_monotone_r.n, m, k: nat
kp: 0 < k
mp: 0 < m
n mod (m * k) < m * k
      napply (nat_mod_lt_r' _ _ 0 _).n, m, k: nat
kp: 0 < k
mp: 0 < m
0 < m * k
      exact (nat_mul_strictly_monotone mp kp).
    -n, m, k: nat
kp: 0 < k
mp: 0 < m
(m * k) / m <= k by rewrite nat_div_mul_cancel_l. }n, m, k: nat
kp: 0 < k
mp: 0 < m
k * (n / (m * k)) + (n mod (m * k)) / m = n / m
  transitivity ((m * (k * (n / (m * k)))) / m + (n mod (m * k)) / m).n, m, k: nat
kp: 0 < k
mp: 0 < m
k * (n / (m * k)) + (n mod (m * k)) / m =
(m * (k * (n / (m * k)))) / m + (n mod (m * k)) / m
n, m, k: nat
kp: 0 < k
mp: 0 < m
(m * (k * (n / (m * k)))) / m + (n mod (m * k)) / m =
n / m
  -n, m, k: nat
kp: 0 < k
mp: 0 < m
k * (n / (m * k)) + (n mod (m * k)) / m =
(m * (k * (n / (m * k)))) / m + (n mod (m * k)) / m f_ap.n, m, k: nat
kp: 0 < k
mp: 0 < m
k * (n / (m * k)) = (m * (k * (n / (m * k)))) / m
    symmetry; rapply nat_div_mul_cancel_l.
  -n, m, k: nat
kp: 0 < k
mp: 0 < m
(m * (k * (n / (m * k)))) / m + (n mod (m * k)) / m =
n / m rewrite nat_mul_assoc.n, m, k: nat
kp: 0 < k
mp: 0 < m
(m * k * (n / (m * k))) / m + (n mod (m * k)) / m =
n / m
    lhs_V napply nat_div_dist.n, m, k: nat
kp: 0 < k
mp: 0 < m
(m | m * k * (n / (m * k)))
n, m, k: nat
kp: 0 < k
mp: 0 < m
(m * k * (n / (m * k)) + n mod (m * k)) / m = n / m
    1: exact _.n, m, k: nat
kp: 0 < k
mp: 0 < m
(m * k * (n / (m * k)) + n mod (m * k)) / m = n / m
    apply (ap (fun x => x / m)).n, m, k: nat
kp: 0 < k
mp: 0 < m
m * k * (n / (m * k)) + n mod (m * k) = n
    symmetry; apply nat_div_mod_spec.
Defined.

(** Dividing a number by a quotient is the same as dividing the product of the number with the denominator of the quotient by the numerator of the quotient. *)
Definition nat_div_div_r 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
  intros [d r].n, m, k, d: nat
r: d * k = m
n / (m / k) = (n * k) / m
  destruct (nat_zero_or_gt_zero k) as [[] | kp].n, m, k, d: nat
r: d * k = m
n / (m / 0) = (n * 0) / m
n, m, k, d: nat
r: d * k = m
kp: 0 < k
n / (m / k) = (n * k) / m
  1: by rewrite nat_mul_zero_r, nat_div_zero_l.n, m, k, d: nat
r: d * k = m
kp: 0 < k
n / (m / k) = (n * k) / m
  destruct r.n, k, d: nat
kp: 0 < k
n / ((d * k) / k) = (n * k) / (d * k)
  rhs napply nat_div_cancel_mul_r.n, k, d: nat
kp: 0 < k
n / ((d * k) / k) = n / d
n, k, d: nat
kp: 0 < k
0 < k
  2: exact _.n, k, d: nat
kp: 0 < k
n / ((d * k) / k) = n / d
  apply ap.n, k, d: nat
kp: 0 < k
(d * k) / k = d
  rapply nat_div_mul_cancel_r.
Defined.

(** A variant of [nat_div_div_r] without the divisibility assumption, by modifying [m] to become divisible. *)
Definition nat_div_div_r' n m k : n / (m / k) = (n * k) / (m - m mod k).n, m, k: nat
n / (m / k) = (n * k) / (m - m mod k)
Proof.n, m, k: nat
n / (m / k) = (n * k) / (m - m mod k)
  rewrite (nat_div_sub_mod m k).n, m, k: nat
n / ((m - m mod k) / k) = (n * k) / (m - m mod k)
  rapply nat_div_div_r.
Defined.

(** We can cancel common factors on the left in a modulo. *)
Definition nat_mod_mul_l n m k
  : (k * n) mod (k * m) = k * (n mod m).n, m, k: nat
(k * n) mod (k * m) = k * (n mod m)
Proof.n, m, k: nat
(k * n) mod (k * m) = k * (n mod m)
  destruct (nat_zero_or_gt_zero k) as [[] | kp].n, m, k: nat
(0 * n) mod (0 * m) = 0 * (n mod m)
n, m, k: nat
kp: 0 < k
(k * n) mod (k * m) = k * (n mod m)
  1: reflexivity.n, m, k: nat
kp: 0 < k
(k * n) mod (k * m) = k * (n mod m)
  destruct (nat_zero_or_gt_zero m) as [[] | mp].n, m, k: nat
kp: 0 < k
(k * n) mod (k * 0) = k * (n mod 0)
n, m, k: nat
kp: 0 < k
mp: 0 < m
(k * n) mod (k * m) = k * (n mod m)
  1: by rewrite nat_mul_zero_r.n, m, k: nat
kp: 0 < k
mp: 0 < m
(k * n) mod (k * m) = k * (n mod m)
  apply (nat_mod_unique _ _ (n / m)).n, m, k: nat
kp: 0 < k
mp: 0 < m
k * (n mod m) < k * m
n, m, k: nat
kp: 0 < k
mp: 0 < m
k * m * (n / m) + k * (n mod m) = k * n
  1: rapply nat_mul_l_strictly_monotone.n, m, k: nat
kp: 0 < k
mp: 0 < m
k * m * (n / m) + k * (n mod m) = k * n
  rewrite <- nat_mul_assoc.n, m, k: nat
kp: 0 < k
mp: 0 < m
k * (m * (n / m)) + k * (n mod m) = k * n
  rewrite <- nat_dist_l.n, m, k: nat
kp: 0 < k
mp: 0 < m
k * (m * (n / m) + n mod m) = k * n
  apply ap.n, m, k: nat
kp: 0 < k
mp: 0 < m
m * (n / m) + n mod m = n
  symmetry; apply nat_div_mod_spec.
Defined.

(** We can cancel common factors on the right in a modulo. *)
Definition nat_mod_mul_r n m k
  : (n * k) mod (m * k) = (n mod m) * k.n, m, k: nat
(n * k) mod (m * k) = n mod m * k
Proof.n, m, k: nat
(n * k) mod (m * k) = n mod m * k
  rewrite 3 (nat_mul_comm _ k).n, m, k: nat
(k * n) mod (k * m) = k * (n mod m)
  napply nat_mod_mul_l.
Defined.

(** We can move a divisor from the right to become a factor on the left of an equation. *)
Definition nat_div_moveL_nV n m k : 0 < k -> n * k = m -> n = m / k.n, m, k: nat
0 < k -> n * k = m -> n = m / k
Proof.n, m, k: nat
0 < k -> n * k = m -> n = m / k
  intros H p.n, m, k: nat
H: 0 < k
p: n * k = m
n = m / k
  destruct p.n, k: nat
H: 0 < k
n = (n * k) / k
  symmetry; rapply nat_div_mul_cancel_r.
Defined.

Definition nat_div_moveR_nV n m k : 0 < k -> n = m * k -> n / k = m.n, m, k: nat
0 < k -> n = m * k -> n / k = m
Proof.n, m, k: nat
0 < k -> n = m * k -> n / k = m
  intros H p.n, m, k: nat
H: 0 < k
p: n = m * k
n / k = m
  destruct p^.m, k: nat
H: 0 < k
p: m * k = m * k
(m * k) / k = m
  rapply nat_div_mul_cancel_r.
Defined.

Definition nat_divides_l_div n m l
  : 0 < m -> (m | n) -> (n | l * m) -> (n / m | l).n, m, l: nat
0 < m -> (m | n) -> (n | l * m) -> (n / m | l)
Proof.n, m, l: nat
0 < m -> (m | n) -> (n | l * m) -> (n / m | l)
  intros H1 H2 [y q].n, m, l: nat
H1: 0 < m
H2: (m | n)
y: nat
q: y * n = l * m
(n / m | l)
  exists y.n, m, l: nat
H1: 0 < m
H2: (m | n)
y: nat
q: y * n = l * m
y * (n / m) = l
  rewrite nat_div_mul_l; only 2: exact _.n, m, l: nat
H1: 0 < m
H2: (m | n)
y: nat
q: y * n = l * m
(y * n) / m = l
  by rapply nat_div_moveR_nV.
Defined.

Definition nat_divides_r_div n m l
  : (n * l | m) -> (n | m / l).n, m, l: nat
(n * l | m) -> (n | m / l)
Proof.n, m, l: nat
(n * l | m) -> (n | m / l)
  destruct l; only 1: exact _.n, m, l: nat
(n * l.+1 | m) -> (n | m / l.+1)
  intros [k p].n, m, l, k: nat
p: k * (n * l.+1) = m
(n | m / l.+1)
  exists k.n, m, l, k: nat
p: k * (n * l.+1) = m
k * n = m / l.+1
  rapply nat_div_moveL_nV.n, m, l, k: nat
p: k * (n * l.+1) = m
k * n * l.+1 = m
  by lhs_V napply nat_mul_assoc.
Defined.

Definition nat_divides_l_mul n m l
  : (l | m) -> (n | m / l) -> (n * l | m).n, m, l: nat
(l | m) -> (n | m / l) -> (n * l | m)
Proof.n, m, l: nat
(l | m) -> (n | m / l) -> (n * l | m)
  intros H [k p].n, m, l: nat
H: (l | m)
k: nat
p: k * n = m / l
(n * l | m)
  exists k.n, m, l: nat
H: (l | m)
k: nat
p: k * n = m / l
k * (n * l) = m
  rewrite nat_mul_assoc.n, m, l: nat
H: (l | m)
k: nat
p: k * n = m / l
k * n * l = m
  rewrite p.n, m, l: nat
H: (l | m)
k: nat
p: k * n = m / l
m / l * l = m
  rapply nat_mul_div_cancel_r.  
Defined.

(** ** Greatest Common Divisor *)

(** The greatest common divisor of [0] and a number is the number itself. *)
Definition nat_gcd_zero_l n : nat_gcd 0 n = n := idpath.

(** The greatest common divisor of a number and [0] is the number itself. *)
Definition nat_gcd_zero_r n : nat_gcd n 0 = n.n: nat
nat_gcd n 0 = n
Proof.n: nat
nat_gcd n 0 = n
  induction n; simpl; only 1: reflexivity.n: nat
IHn: nat_gcd n 0 = n
nat_gcd (n - n) n.+1 = n.+1
  by rewrite nat_sub_cancel.
Defined.

(** The greatest common divisor of [1] and any number is [1]. *)
Definition nat_gcd_one_l n : nat_gcd 1 n = 1 := idpath.

(** The greatest common divisor of any number and [1] is [1]. *)
Definition nat_gcd_one_r n : nat_gcd n 1 = 1.n: nat
nat_gcd n 1 = 1
Proof.n: nat
nat_gcd n 1 = 1
  destruct n; trivial.n: nat
nat_gcd n.+1 1 = 1
  simpl.n: nat
nat_gcd
  (n -
   snd
     match n with
     | 0 => (1, n)
     | u'.+1 => (0, u')
     end) n.+1 = 1
  destruct n; trivial.n: nat
nat_gcd (n.+1 - snd (0, n)) n.+2 = 1
  rewrite nat_sub_succ_l; only 2: exact _.n: nat
nat_gcd (n - snd (0, n)).+1 n.+2 = 1
  by rewrite nat_sub_cancel.
Defined.

(** Idempotency. *)
Definition nat_gcd_idem n : nat_gcd n n = n.n: nat
nat_gcd n n = n
Proof.n: nat
nat_gcd n n = n
  induction n.nat_gcd 0 0 = 0
n: nat
IHn: nat_gcd n n = n
nat_gcd n.+1 n.+1 = n.+1
  1: reflexivity.n: nat
IHn: nat_gcd n n = n
nat_gcd n.+1 n.+1 = n.+1
  unfold nat_gcd; fold nat_gcd.n: nat
IHn: nat_gcd n n = n
nat_gcd (n.+1 mod n.+1) n.+1 = n.+1
  by rewrite nat_mod_cancel.
Defined.

(** We can prove that the greatest common divisor of [n] and [m] divides both [n] and [m]. This proof requires strong induction. *)
Definition nat_divides_l_gcd n m : (nat_gcd n m | n) /\ (nat_gcd n m | m).n, m: nat
((nat_gcd n m | n) * (nat_gcd n m | m))%type
Proof.n, m: nat
((nat_gcd n m | n) * (nat_gcd n m | m))%type
  revert n m; snapply nat_ind_strong; intros n IHn m.n: nat
IHn: forall m : nat,
m < n ->
(fun n : nat => forall m0 : nat, (nat_gcd n m0 | n) * (nat_gcd n m0 | m0)) m
m: nat
((nat_gcd n m | n) * (nat_gcd n m | m))%type
  destruct n.IHn: forall m : nat,
m < 0 -> forall m0 : nat, (nat_gcd m m0 | m) * (nat_gcd m m0 | m0)
m: nat
((nat_gcd 0 m | 0) * (nat_gcd 0 m | m))%type
n: nat
IHn: forall m : nat,
m < n.+1 -> forall m0 : nat, (nat_gcd m m0 | m) * (nat_gcd m m0 | m0)
m: nat
((nat_gcd n.+1 m | n.+1) * (nat_gcd n.+1 m | m))%type
  1: split; exact _.n: nat
IHn: forall m : nat,
m < n.+1 -> forall m0 : nat, (nat_gcd m m0 | m) * (nat_gcd m m0 | m0)
m: nat
((nat_gcd n.+1 m | n.+1) * (nat_gcd n.+1 m | m))%type
  destruct (IHn (m mod n.+1) _ n.+1) as [H1 H2].n: nat
IHn: forall m : nat,
m < n.+1 -> forall m0 : nat, (nat_gcd m m0 | m) * (nat_gcd m m0 | m0)
m: nat
H1: (nat_gcd (m mod n.+1) n.+1 | m mod n.+1)
H2: (nat_gcd (m mod n.+1) n.+1 | n.+1)
((nat_gcd n.+1 m | n.+1) * (nat_gcd n.+1 m | m))%type
  unfold nat_gcd; fold nat_gcd.n: nat
IHn: forall m : nat,
m < n.+1 -> forall m0 : nat, (nat_gcd m m0 | m) * (nat_gcd m m0 | m0)
m: nat
H1: (nat_gcd (m mod n.+1) n.+1 | m mod n.+1)
H2: (nat_gcd (m mod n.+1) n.+1 | n.+1)
((nat_gcd (m mod n.+1) n.+1 | n.+1) *
 (nat_gcd (m mod n.+1) n.+1 | m))%type
  set (n' := n.+1) in *.n: nat
n':= n.+1: nat
IHn: forall m : nat,
m < n' -> forall m0 : nat, (nat_gcd m m0 | m) * (nat_gcd m m0 | m0)
m: nat
H1: (nat_gcd (m mod n') n' | m mod n')
H2: (nat_gcd (m mod n') n' | n')
((nat_gcd (m mod n') n' | n') *
 (nat_gcd (m mod n') n' | m))%type
  split; only 1: exact H2.n: nat
n':= n.+1: nat
IHn: forall m : nat,
m < n' -> forall m0 : nat, (nat_gcd m m0 | m) * (nat_gcd m m0 | m0)
m: nat
H1: (nat_gcd (m mod n') n' | m mod n')
H2: (nat_gcd (m mod n') n' | n')
(nat_gcd (m mod n') n' | m)
  set (r := m mod n'); rewrite (nat_div_mod_spec m n'); unfold r; clear r.n: nat
n':= n.+1: nat
IHn: forall m : nat,
m < n' -> forall m0 : nat, (nat_gcd m m0 | m) * (nat_gcd m m0 | m0)
m: nat
H1: (nat_gcd (m mod n') n' | m mod n')
H2: (nat_gcd (m mod n') n' | n')
(nat_gcd (m mod n') n' | n' * (m / n') + m mod n')
  exact _.
Defined.

(** The greatest common divisor of [n] and [m] divides [n]. *)
Instance nat_divides_l_gcd_l n m : (nat_gcd n m | n)
  := fst (nat_divides_l_gcd n m).

(** The greatest common divisor of [n] and [m] divides [m]. *)
Instance divides_l_nat_gcd_r n m : (nat_gcd n m | m)
  := snd (nat_divides_l_gcd n m).

(** We can prove that any common divisor of [n] and [m] divides the greatest common divisor of [n] and [m]. It is in that sense the greatest. *)
Instance nat_divides_r_gcd n m p : (p | n) -> (p | m) -> (p | nat_gcd n m).n, m, p: nat
(p | n) -> (p | m) -> (p | nat_gcd n m)
Proof.n, m, p: nat
(p | n) -> (p | m) -> (p | nat_gcd n m)
  revert n m p; snapply nat_ind_strong; intros n IHn m p H1 H2.n: nat
IHn: forall m : nat,
m < n ->
(fun n : nat => forall m0 p : nat, (p | n) -> (p | m0) -> (p | nat_gcd n m0))
m
m, p: nat
H1: (p | n)
H2: (p | m)
(p | nat_gcd n m)
  destruct n; only 1: exact _.n: nat
IHn: forall m : nat,
m < n.+1 -> forall m0 p : nat, (p | m) -> (p | m0) -> (p | nat_gcd m m0)
m, p: nat
H1: (p | n.+1)
H2: (p | m)
(p | nat_gcd n.+1 m)
  unfold nat_gcd; fold nat_gcd.n: nat
IHn: forall m : nat,
m < n.+1 -> forall m0 p : nat, (p | m) -> (p | m0) -> (p | nat_gcd m m0)
m, p: nat
H1: (p | n.+1)
H2: (p | m)
(p | nat_gcd (m mod n.+1) n.+1)
  apply IHn; only 1,3: exact _.n: nat
IHn: forall m : nat,
m < n.+1 -> forall m0 p : nat, (p | m) -> (p | m0) -> (p | nat_gcd m m0)
m, p: nat
H1: (p | n.+1)
H2: (p | m)
(p | m mod n.+1)
  rewrite (nat_div_mod_spec m n.+1) in H2.n: nat
IHn: forall m : nat,
m < n.+1 -> forall m0 p : nat, (p | m) -> (p | m0) -> (p | nat_gcd m m0)
m, p: nat
H1: (p | n.+1)
H2: (p | n.+1 * (m / n.+1) + m mod n.+1)
(p | m mod n.+1)
  apply nat_divides_add_r in H2; exact _.
Defined.

Definition nat_divides_r_iff_divides_r_gcd n m p
  : (p | n) * (p | m) <-> (p | nat_gcd n m).n, m, p: nat
(p | n) * (p | m) <-> (p | nat_gcd n m)
Proof.n, m, p: nat
(p | n) * (p | m) <-> (p | nat_gcd n m)
  split; [intros [H1 H2] | intros H; split]; exact _.
Defined.

(** If [p] is divisible by all common divisors of [n] and [m], and [p] is also a common divisor, then it must necessarily be equal to the greatest common divisor. *)
Definition nat_gcd_unique n m p
  (H : forall q, (q | n) -> (q | m) -> (q | p))
  : (p | n) -> (p | m) -> nat_gcd n m = p.n, m, p: nat
H: forall q : nat, (q | n) -> (q | m) -> (q | p)
(p | n) -> (p | m) -> nat_gcd n m = p
Proof.n, m, p: nat
H: forall q : nat, (q | n) -> (q | m) -> (q | p)
(p | n) -> (p | m) -> nat_gcd n m = p
  intros H1 H2.n, m, p: nat
H: forall q : nat, (q | n) -> (q | m) -> (q | p)
H1: (p | n)
H2: (p | m)
nat_gcd n m = p
  rapply nat_divides_antisym.
Defined.

(** As a corollary of uniqueness, we get that the greatest common divisor operation is commutative. *)
Definition nat_gcd_comm n m : nat_gcd n m = nat_gcd m n.n, m: nat
nat_gcd n m = nat_gcd m n
Proof.n, m: nat
nat_gcd n m = nat_gcd m n
  rapply nat_gcd_unique.
Defined.

(** [nat_gcd] is associative. *)
Definition nat_gcd_assoc n m k : nat_gcd n (nat_gcd m k) = nat_gcd (nat_gcd n m) k.n, m, k: nat
nat_gcd n (nat_gcd m k) = nat_gcd (nat_gcd n m) k
Proof.n, m, k: nat
nat_gcd n (nat_gcd m k) = nat_gcd (nat_gcd n m) k
  rapply nat_gcd_unique.n, m, k: nat
(nat_gcd (nat_gcd n m) k | n)
n, m, k: nat
(nat_gcd (nat_gcd n m) k | nat_gcd m k)
  -n, m, k: nat
(nat_gcd (nat_gcd n m) k | n) rapply (nat_divides_trans (nat_divides_l_gcd_l _ _)).
  -n, m, k: nat
(nat_gcd (nat_gcd n m) k | nat_gcd m k) apply nat_divides_r_gcd; rapply nat_divides_trans.
Defined.

(** If [nat_gcd n m] is [0], then [n] must also be [0]. *)
Definition nat_gcd_is_zero_l n m : nat_gcd n m = 0 -> n = 0.n, m: nat
nat_gcd n m = 0 -> n = 0
Proof.n, m: nat
nat_gcd n m = 0 -> n = 0
  intros H.n, m: nat
H: nat_gcd n m = 0
n = 0
  generalize (nat_divides_l_gcd_l n m).n, m: nat
H: nat_gcd n m = 0
(nat_gcd n m | n) -> n = 0
  rewrite H.n, m: nat
H: nat_gcd n m = 0
(0 | n) -> n = 0
  intros [x p].n, m: nat
H: nat_gcd n m = 0
x: nat
p: x * 0 = n
n = 0
  exact (p^ @ nat_mul_zero_r _).
Defined.

(** If [nat_gcd n m] is [0], then [m] must also be [0]. *)
Definition nat_gcd_is_zero_r n m : nat_gcd n m = 0 -> m = 0.n, m: nat
nat_gcd n m = 0 -> m = 0
Proof.n, m: nat
nat_gcd n m = 0 -> m = 0
  rewrite nat_gcd_comm.n, m: nat
nat_gcd m n = 0 -> m = 0
  apply nat_gcd_is_zero_l.
Defined.

(** [nat_gcd n m] is [0] if and only if both [n] and [m] are [0]. *)
Definition nat_gcd_zero_iff_zero n m : nat_gcd n m = 0 <-> n = 0 /\ m = 0.n, m: nat
nat_gcd n m = 0 <-> (n = 0) * (m = 0)
Proof.n, m: nat
nat_gcd n m = 0 <-> (n = 0) * (m = 0)
  split.n, m: nat
nat_gcd n m = 0 -> (n = 0) * (m = 0)
n, m: nat
(n = 0) * (m = 0) -> nat_gcd n m = 0
  -n, m: nat
nat_gcd n m = 0 -> (n = 0) * (m = 0) split.n, m: nat
H: nat_gcd n m = 0
n = 0
n, m: nat
H: nat_gcd n m = 0
m = 0
    +n, m: nat
H: nat_gcd n m = 0
n = 0 by apply (nat_gcd_is_zero_l _ m).
    +n, m: nat
H: nat_gcd n m = 0
m = 0 by apply (nat_gcd_is_zero_r n).
  -n, m: nat
(n = 0) * (m = 0) -> nat_gcd n m = 0 intros [-> ->].nat_gcd 0 0 = 0
    reflexivity.
Defined.

(** [nat_gcd] is positive for positive inputs. *)
Instance nat_gcd_pos n m : 0 < n -> 0 < m -> 0 < nat_gcd n m.n, m: nat
0 < n -> 0 < m -> 0 < nat_gcd n m
Proof.n, m: nat
0 < n -> 0 < m -> 0 < nat_gcd n m
  intros H1 H2.n, m: nat
H1: 0 < n
H2: 0 < m
0 < nat_gcd n m
  apply lt_iff_not_geq.n, m: nat
H1: 0 < n
H2: 0 < m
~ (0 >= nat_gcd n m)
  intros H3; hnf in H3.n, m: nat
H1: 0 < n
H2: 0 < m
H3: nat_gcd n m <= 0
Empty
  apply path_zero_leq_zero_r in H3.n, m: nat
H1: 0 < n
H2: 0 < m
H3: nat_gcd n m = 0
Empty
  apply nat_gcd_zero_iff_zero in H3.n, m: nat
H1: 0 < n
H2: 0 < m
H3: ((n = 0) * (m = 0))%type
Empty
  destruct H3 as [->].m: nat
H1: 0 < 0
H2: 0 < m
snd: m = 0
Empty
  contradiction (not_lt_zero_r _ H1).
Defined.

Definition nat_gcd_l_add_r_mul n m k : nat_gcd (n + k * m) m = nat_gcd n m.n, m, k: nat
nat_gcd (n + k * m) m = nat_gcd n m
Proof.n, m, k: nat
nat_gcd (n + k * m) m = nat_gcd n m
  rapply nat_gcd_unique.n, m, k: nat
forall q : nat,
(q | n + k * m) -> (q | m) -> (q | nat_gcd n m)
  intros q H1 H2.n, m, k, q: nat
H1: (q | n + k * m)
H2: (q | m)
(q | nat_gcd n m)
  rapply nat_divides_r_gcd.n, m, k, q: nat
H1: (q | n + k * m)
H2: (q | m)
(q | n)
  rapply (nat_divides_add_l _ _ (k * m)).
Defined.

Definition nat_gcd_r_add_r_mul n m k : nat_gcd n (m + k * n) = nat_gcd n m.n, m, k: nat
nat_gcd n (m + k * n) = nat_gcd n m
Proof.n, m, k: nat
nat_gcd n (m + k * n) = nat_gcd n m
  lhs napply nat_gcd_comm.n, m, k: nat
nat_gcd (m + k * n) n = nat_gcd n m
  rhs napply nat_gcd_comm.n, m, k: nat
nat_gcd (m + k * n) n = nat_gcd m n
  napply nat_gcd_l_add_r_mul.
Defined.

Definition nat_gcd_l_add_r n m : nat_gcd (n + m) m = nat_gcd n m.n, m: nat
nat_gcd (n + m) m = nat_gcd n m
Proof.n, m: nat
nat_gcd (n + m) m = nat_gcd n m
  rhs_V exact (nat_gcd_l_add_r_mul n m 1).n, m: nat
nat_gcd (n + m) m = nat_gcd (n + 1 * m) m
  by rewrite nat_mul_one_l.
Defined.

Definition nat_gcd_r_add_r n m : nat_gcd n (m + n) = nat_gcd n m.n, m: nat
nat_gcd n (m + n) = nat_gcd n m
Proof.n, m: nat
nat_gcd n (m + n) = nat_gcd n m
  lhs napply nat_gcd_comm.n, m: nat
nat_gcd (m + n) n = nat_gcd n m
  rhs napply nat_gcd_comm.n, m: nat
nat_gcd (m + n) n = nat_gcd m n
  napply nat_gcd_l_add_r.
Defined.

Definition nat_gcd_l_sub n m : m <= n -> nat_gcd (n - m) m = nat_gcd n m.n, m: nat
m <= n -> nat_gcd (n - m) m = nat_gcd n m
Proof.n, m: nat
m <= n -> nat_gcd (n - m) m = nat_gcd n m
  intros H.n, m: nat
H: m <= n
nat_gcd (n - m) m = nat_gcd n m
  lhs_V napply nat_gcd_l_add_r.n, m: nat
H: m <= n
nat_gcd (n - m + m) m = nat_gcd n m
  by rewrite (nat_add_sub_l_cancel H).
Defined.

Definition nat_gcd_r_sub n m : n <= m -> nat_gcd n (m - n) = nat_gcd n m.n, m: nat
n <= m -> nat_gcd n (m - n) = nat_gcd n m
Proof.n, m: nat
n <= m -> nat_gcd n (m - n) = nat_gcd n m
  intros H.n, m: nat
H: n <= m
nat_gcd n (m - n) = nat_gcd n m
  lhs napply nat_gcd_comm.n, m: nat
H: n <= m
nat_gcd (m - n) n = nat_gcd n m
  rhs napply nat_gcd_comm.n, m: nat
H: n <= m
nat_gcd (m - n) n = nat_gcd m n
  rapply nat_gcd_l_sub.
Defined.

(** ** Bezout's Identity *)

(** Bezout's identity states that for any two numbers [n] and [m], their greatest common divisor can be written as a linear combination of [n] and [m]. This is easy to state for the integers, however since we are working with the natural numbers, we need to be more careful. This is why we write the linear combination as [a * n = d + b * m] rather than the usual [a * n + b * m = d]. *)

(** We define a predicate for triples of integers satisfying Bezout's identity. *)
Definition NatBezout n m d : Type0
  := exists a b, a * n = d + b * m.
Existing Class NatBezout.

Instance nat_bezout_refl_l n k : NatBezout n k n.n, k: nat
NatBezout n k n
Proof.n, k: nat
NatBezout n k n
  by exists 1, 0.
Defined.

(** If [a * n = 1 + b * m], then the gcd of [n] and [m] is [1]. *)
Definition nat_bezout_coprime n m : NatBezout n m 1 -> nat_gcd n m = 1.n, m: nat
NatBezout n m 1 -> nat_gcd n m = 1
Proof.n, m: nat
NatBezout n m 1 -> nat_gcd n m = 1
  intros [a [b p]].n, m, a, b: nat
p: a * n = 1 + b * m
nat_gcd n m = 1
  rapply nat_gcd_unique.n, m, a, b: nat
p: a * n = 1 + b * m
forall q : nat, (q | n) -> (q | m) -> (q | 1)
  intros q H1 H2.n, m, a, b: nat
p: a * n = 1 + b * m
q: nat
H1: (q | n)
H2: (q | m)
(q | 1)
  rapply (nat_divides_add_l _ _ (b * m)).n, m, a, b: nat
p: a * n = 1 + b * m
q: nat
H1: (q | n)
H2: (q | m)
(q | 1 + b * m)
  destruct p; exact _.
Defined.

Definition nat_bezout_comm n m d
  : 0 < m -> NatBezout n m d -> NatBezout m n d.n, m, d: nat
0 < m -> NatBezout n m d -> NatBezout m n d
Proof.n, m, d: nat
0 < m -> NatBezout n m d -> NatBezout m n d
  intros H [a [b p]].n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
NatBezout m n d
  destruct (@equiv_leq_lt_or_eq 0 a _) as [|q].n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
NatBezout m n d
n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
q: 0 = a
NatBezout m n d
  -n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
NatBezout m n d exists (n * a.+1 * b.+1 - b), (m * a.+1 * b.+1 - a).n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
(n * a.+1 * b.+1 - b) * m =
d + (m * a.+1 * b.+1 - a) * n
    rewrite 2 nat_dist_sub_r.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
n * a.+1 * b.+1 * m - b * m =
d + (m * a.+1 * b.+1 * n - a * n)
    apply nat_moveR_nV.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
n * a.+1 * b.+1 * m =
d + (m * a.+1 * b.+1 * n - a * n) + b * m
    rewrite <- nat_add_comm, nat_add_assoc, <- (nat_add_comm d).n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
n * a.+1 * b.+1 * m =
d + b * m + (m * a.+1 * b.+1 * n - a * n)
    rewrite <- nat_sub_l_add_r.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
n * a.+1 * b.+1 * m =
d + b * m + m * a.+1 * b.+1 * n - a * n
n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
a * n <= m * a.+1 * b.+1 * n
    2: {n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
a * n <= m * a.+1 * b.+1 * n apply nat_mul_r_monotone.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
a <= m * a.+1 * b.+1
      rewrite 2 nat_mul_succ_r.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
a <= (m * a + m) * b + (m * a + m)
      napply (leq_trans _ (leq_add_l _ _)).n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
a <= m * a + m
      exact (leq_trans _ (leq_add_r _ _)). }n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
n * a.+1 * b.+1 * m =
d + b * m + m * a.+1 * b.+1 * n - a * n
    apply nat_moveL_nV.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
n * a.+1 * b.+1 * m + a * n =
d + b * m + m * a.+1 * b.+1 * n
    rewrite nat_add_comm.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
a * n + n * a.+1 * b.+1 * m =
d + b * m + m * a.+1 * b.+1 * n
    snapply (ap011 nat_add p).n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
n * a.+1 * b.+1 * m = m * a.+1 * b.+1 * n
    lhs napply nat_mul_comm.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
m * (n * a.+1 * b.+1) = m * a.+1 * b.+1 * n
    rhs_V napply nat_mul_assoc.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
m * (n * a.+1 * b.+1) = m * a.+1 * (b.+1 * n)
    rhs_V napply nat_mul_assoc.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
m * (n * a.+1 * b.+1) = m * (a.+1 * (b.+1 * n))
    snapply ap.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
n * a.+1 * b.+1 = a.+1 * (b.+1 * n)
    lhs_V napply nat_mul_assoc.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
n * (a.+1 * b.+1) = a.+1 * (b.+1 * n)
    rhs napply nat_mul_assoc.n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
l: 0 < a
n * (a.+1 * b.+1) = a.+1 * b.+1 * n
    apply nat_mul_comm.
  -n, m, d: nat
H: 0 < m
a, b: nat
p: a * n = d + b * m
q: 0 = a
NatBezout m n d destruct q.n, m, d: nat
H: 0 < m
b: nat
p: 0 * n = d + b * m
NatBezout m n d
    exists 0, 0.n, m, d: nat
H: 0 < m
b: nat
p: 0 * n = d + b * m
0 * m = d + 0 * n
    rewrite 2 nat_mul_zero_l, nat_add_zero_r in *.n, m, d: nat
H: 0 < m
b: nat
p: 0 = d + b * m
0 = d
    symmetry in p; symmetry.n, m, d: nat
H: 0 < m
b: nat
p: d + b * m = 0
d = 0
    apply equiv_nat_add_zero in p.n, m, d: nat
H: 0 < m
b: nat
p: ((d = 0) * ((b * m)%nat = 0))%type
d = 0
    by destruct p.
Defined.
Hint Immediate nat_bezout_comm : typeclass_instances.

Instance nat_bezout_pos_l n m : 0 < n -> NatBezout n m (nat_gcd n m).n, m: nat
0 < n -> NatBezout n m (nat_gcd n m)
Proof.n, m: nat
0 < n -> NatBezout n m (nat_gcd n m)
  pose (k := n + m); assert (p : n + m = k) by reflexivity; clearbody k.n, m, k: nat
p: n + m = k
0 < n -> NatBezout n m (nat_gcd n m)
  revert k n m p; snapply nat_ind_strong; hnf; intros k IHk n m q H.k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
NatBezout n m (nat_gcd n m)
  (** Given a sum [n + m], we can always find another pair [n' + m'] equal to that sum such that [n' < m']. This extra hypothesis lets us prove the statement more directly. *)
  assert (H' : forall n' m', n + m = n' + m' -> 0 < n' -> n' < m'
    -> NatBezout n' m' (nat_gcd n' m')).k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
forall n' m' : nat,
n + m = n' + m' ->
0 < n' -> n' < m' -> NatBezout n' m' (nat_gcd n' m')
k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
NatBezout n m (nat_gcd n m)
  {k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
forall n' m' : nat,
n + m = n' + m' ->
0 < n' -> n' < m' -> NatBezout n' m' (nat_gcd n' m') intros n' m' p H1 H2; destruct q.n, m: nat
IHk: forall m0 : nat,
m0 < n + m ->
forall n m : nat, n + m = m0 -> 0 < n -> NatBezout n m (nat_gcd n m)
H: 0 < n
n', m': nat
p: n + m = n' + m'
H1: 0 < n'
H2: n' < m'
NatBezout n' m' (nat_gcd n' m')
    assert (m' < n + m) by (rewrite p; change (0 + m' < n' + m'); exact _).n, m: nat
IHk: forall m0 : nat,
m0 < n + m ->
forall n m : nat, n + m = m0 -> 0 < n -> NatBezout n m (nat_gcd n m)
H: 0 < n
n', m': nat
p: n + m = n' + m'
H1: 0 < n'
H2: n' < m'
H0: m' < n + m
NatBezout n' m' (nat_gcd n' m')
    destruct (IHk m' _ n' (m' - n') (nat_add_sub_r_cancel _) _) as [a [b r]].n, m: nat
IHk: forall m0 : nat,
m0 < n + m ->
forall n m : nat, n + m = m0 -> 0 < n -> NatBezout n m (nat_gcd n m)
H: 0 < n
n', m': nat
p: n + m = n' + m'
H1: 0 < n'
H2: n' < m'
H0: m' < n + m
a, b: nat
r: a * n' = nat_gcd n' (m' - n') + b * (m' - n')
NatBezout n' m' (nat_gcd n' m')
    exists (a + b), b.n, m: nat
IHk: forall m0 : nat,
m0 < n + m ->
forall n m : nat, n + m = m0 -> 0 < n -> NatBezout n m (nat_gcd n m)
H: 0 < n
n', m': nat
p: n + m = n' + m'
H1: 0 < n'
H2: n' < m'
H0: m' < n + m
a, b: nat
r: a * n' = nat_gcd n' (m' - n') + b * (m' - n')
(a + b) * n' = nat_gcd n' m' + b * m'
    rewrite nat_dist_r, r, nat_dist_sub_l, <- nat_add_assoc.n, m: nat
IHk: forall m0 : nat,
m0 < n + m ->
forall n m : nat, n + m = m0 -> 0 < n -> NatBezout n m (nat_gcd n m)
H: 0 < n
n', m': nat
p: n + m = n' + m'
H1: 0 < n'
H2: n' < m'
H0: m' < n + m
a, b: nat
r: a * n' = nat_gcd n' (m' - n') + b * (m' - n')
nat_gcd n' (m' - n') + (b * m' - b * n' + b * n') =
nat_gcd n' m' + b * m'
    rewrite nat_add_sub_l_cancel; only 2: rapply nat_mul_l_monotone.n, m: nat
IHk: forall m0 : nat,
m0 < n + m ->
forall n m : nat, n + m = m0 -> 0 < n -> NatBezout n m (nat_gcd n m)
H: 0 < n
n', m': nat
p: n + m = n' + m'
H1: 0 < n'
H2: n' < m'
H0: m' < n + m
a, b: nat
r: a * n' = nat_gcd n' (m' - n') + b * (m' - n')
nat_gcd n' (m' - n') + b * m' = nat_gcd n' m' + b * m'
    snapply (ap (fun x => x + _)).n, m: nat
IHk: forall m0 : nat,
m0 < n + m ->
forall n m : nat, n + m = m0 -> 0 < n -> NatBezout n m (nat_gcd n m)
H: 0 < n
n', m': nat
p: n + m = n' + m'
H1: 0 < n'
H2: n' < m'
H0: m' < n + m
a, b: nat
r: a * n' = nat_gcd n' (m' - n') + b * (m' - n')
nat_gcd n' (m' - n') = nat_gcd n' m'
    rapply nat_gcd_r_sub. }k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
NatBezout n m (nat_gcd n m)
  destruct (nat_trichotomy n m) as [[l | p] | r].k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
l: n < m
NatBezout n m (nat_gcd n m)
k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
p: n = m
NatBezout n m (nat_gcd n m)
k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
r: n > m
NatBezout n m (nat_gcd n m)
  -k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
l: n < m
NatBezout n m (nat_gcd n m) by apply H'.
  -k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
p: n = m
NatBezout n m (nat_gcd n m) destruct p.k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n: nat
q: n + n = k
H: 0 < n
H': forall n' m' : nat,
n + n = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
NatBezout n n (nat_gcd n n)
    rewrite nat_gcd_idem; exact _.
  -k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
r: n > m
NatBezout n m (nat_gcd n m) destruct (@equiv_leq_lt_or_eq 0 m _).k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
r: n > m
l: 0 < m
NatBezout n m (nat_gcd n m)
k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
r: n > m
p: 0 = m
NatBezout n m (nat_gcd n m)
    +k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
r: n > m
l: 0 < m
NatBezout n m (nat_gcd n m) rewrite nat_gcd_comm.k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
r: n > m
l: 0 < m
NatBezout n m (nat_gcd m n)
      rapply nat_bezout_comm.k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
r: n > m
l: 0 < m
NatBezout m n (nat_gcd m n)
      rapply H'.k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
r: n > m
l: 0 < m
n + m = m + n
      apply nat_add_comm.
    +k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n, m: nat
q: n + m = k
H: 0 < n
H': forall n' m' : nat,
n + m = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
r: n > m
p: 0 = m
NatBezout n m (nat_gcd n m) destruct p.k: nat
IHk: forall m : nat,
m < k ->
forall n m0 : nat, n + m0 = m -> 0 < n -> NatBezout n m0 (nat_gcd n m0)
n: nat
q: n + 0 = k
H: 0 < n
H': forall n' m' : nat,
n + 0 = n' + m' ->
0 < n' ->
n' < m' -> NatBezout n' m' (nat_gcd n' m')
r: n > 0
NatBezout n 0 (nat_gcd n 0)
      rewrite nat_gcd_zero_r; exact _.
Defined.

(** For strictly positive numbers, we have Bezout's identity in both directions. *)
Definition nat_bezout_pos n m
  : 0 < n -> 0 < m
  -> NatBezout n m (nat_gcd n m) /\ NatBezout m n (nat_gcd n m).n, m: nat
0 < n ->
0 < m ->
NatBezout n m (nat_gcd n m) *
NatBezout m n (nat_gcd n m)
Proof.n, m: nat
0 < n ->
0 < m ->
NatBezout n m (nat_gcd n m) *
NatBezout m n (nat_gcd n m)
  intros H1 H2; split; [| apply nat_bezout_comm]; exact _.
Defined.

(** For arbitrary natural numbers, we have Bezout's identity in at least one direction. *)
Definition nat_bezout n m
  : NatBezout n m (nat_gcd n m) + NatBezout m n (nat_gcd n m).n, m: nat
(NatBezout n m (nat_gcd n m) +
 NatBezout m n (nat_gcd n m))%type
Proof.n, m: nat
(NatBezout n m (nat_gcd n m) +
 NatBezout m n (nat_gcd n m))%type
  destruct n; [ right | left ]; exact _.
Defined.

(** ** Least common multiple *)

(** The least common multiple [nat_lcm n m] is the smallest natural number divisibile by both [n] and [m]. *)
Definition nat_lcm (n m : nat) : nat := n * (m / nat_gcd n m).

(** The least common multiple of [0] and [n] is [0]. *)
Definition nat_lcm_zero_l n : nat_lcm 0 n = 0 := idpath.

(** The least common multiple of [n] and [0] is [0]. *)
Definition nat_lcm_zero_r n : nat_lcm n 0 = 0.n: nat
nat_lcm n 0 = 0
Proof.n: nat
nat_lcm n 0 = 0
  unfold nat_lcm.n: nat
n * (0 / nat_gcd n 0) = 0
  by rewrite nat_div_zero_l, nat_mul_zero_r.
Defined.

(** The least common multiple of [1] and [n] is [n]. *)
Definition nat_lcm_one_l n : nat_lcm 1 n = n.n: nat
nat_lcm 1 n = n
Proof.n: nat
nat_lcm 1 n = n
  unfold nat_lcm.n: nat
1 * (n / nat_gcd 1 n) = n
  by rewrite nat_gcd_one_l, nat_div_one_r, nat_mul_one_l.
Defined.

(** The least common multiple of [n] and [1] is [n]. *)
Definition nat_lcm_one_r n : nat_lcm n 1 = n.n: nat
nat_lcm n 1 = n
Proof.n: nat
nat_lcm n 1 = n
  unfold nat_lcm.n: nat
n * (1 / nat_gcd n 1) = n
  by rewrite nat_gcd_one_r, nat_div_one_r, nat_mul_one_r.
Defined.

(** Idempotency. *)
Definition nat_lcm_idem n : nat_lcm n n = n.n: nat
nat_lcm n n = n
Proof.n: nat
nat_lcm n n = n
  unfold nat_lcm.n: nat
n * (n / nat_gcd n n) = n
  by rewrite nat_gcd_idem, nat_mul_div_cancel_l.
Defined.

(** [n] divides the least common multiple of [n] and [m]. *) 
Instance nat_divides_r_lcm_l n m : (n | nat_lcm n m) := _.

(** [m] divides the least common multiple of [n] and [m]. *)
Instance nat_divides_r_lcm_r n m : (m | nat_lcm n m).n, m: nat
(m | nat_lcm n m)
Proof.n, m: nat
(m | nat_lcm n m)
  unfold nat_lcm.n, m: nat
(m | n * (m / nat_gcd n m))
  rewrite nat_div_mul_l; only 2: exact _.n, m: nat
(m | (n * m) / nat_gcd n m)
  rewrite <- nat_div_mul_r; exact _.
Defined.

(** The least common multiple of [n] and [m] divides any multiple of [n] and [m]. *)
Instance nat_divides_l_lcm n m k : (n | k) -> (m | k) -> (nat_lcm n m | k).n, m, k: nat
(n | k) -> (m | k) -> (nat_lcm n m | k)
Proof.n, m, k: nat
(n | k) -> (m | k) -> (nat_lcm n m | k)
  intros H1 H2.n, m, k: nat
H1: (n | k)
H2: (m | k)
(nat_lcm n m | k)
  destruct (equiv_leq_lt_or_eq (n:=0) (m:=n) _) as [lt_n | p];
    only 2: by destruct p.n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
(nat_lcm n m | k)
  destruct (equiv_leq_lt_or_eq (n:=0) (m:=m) _) as [lt_m | q];
    only 2: (destruct q; by rewrite nat_lcm_zero_r).n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
(nat_lcm n m | k)
  unfold nat_lcm.n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
(n * (m / nat_gcd n m) | k)
  destruct (nat_bezout_pos_l n m _) as [a [b p]].n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
p: a * n = nat_gcd n m + b * m
(n * (m / nat_gcd n m) | k)
  apply nat_moveR_nV in p.n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
p: a * n - b * m = nat_gcd n m
(n * (m / nat_gcd n m) | k)
  rewrite nat_div_mul_l.n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
p: a * n - b * m = nat_gcd n m
((n * m) / nat_gcd n m | k)
n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
p: a * n - b * m = nat_gcd n m
(nat_gcd n m | m)
  2: exact _.n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
p: a * n - b * m = nat_gcd n m
((n * m) / nat_gcd n m | k)
  rapply nat_divides_l_div.n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
p: a * n - b * m = nat_gcd n m
(n * m | k * nat_gcd n m)
  destruct p.n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
(n * m | k * (a * n - b * m))
  rewrite nat_dist_sub_l.n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
(n * m | k * (a * n) - k * (b * m))
  napply nat_divides_sub.n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
(n * m | k * (a * n))
n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
(n * m | k * (b * m))
  1: rewrite nat_mul_comm.n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
(m * n | k * (a * n))
n, m, k: nat
H1: (n | k)
H2: (m | k)
lt_n: 0 < n
lt_m: 0 < m
a, b: nat
(n * m | k * (b * m))
  1,2: exact _.
Defined.

Definition nat_divides_l_iff_divides_l_lcm n m k
  : (n | k) * (m | k) <-> (nat_lcm n m | k).n, m, k: nat
(n | k) * (m | k) <-> (nat_lcm n m | k)
Proof.n, m, k: nat
(n | k) * (m | k) <-> (nat_lcm n m | k)
  split.n, m, k: nat
(n | k) * (m | k) -> (nat_lcm n m | k)
n, m, k: nat
(nat_lcm n m | k) -> (n | k) * (m | k)
  -n, m, k: nat
(n | k) * (m | k) -> (nat_lcm n m | k) intros [H1 H2]; exact _.
  -n, m, k: nat
(nat_lcm n m | k) -> (n | k) * (m | k) intros H; split.n, m, k: nat
H: (nat_lcm n m | k)
(n | k)
n, m, k: nat
H: (nat_lcm n m | k)
(m | k)
    +n, m, k: nat
H: (nat_lcm n m | k)
(n | k) rapply (nat_divides_trans _ H).
    +n, m, k: nat
H: (nat_lcm n m | k)
(m | k) exact _.
Defined.

(** If [k] divides all common multiples of [n] and [m], and [k] is also a common multiple, then it must necessarily be equal to the least common multiple. *)
Definition nat_lcm_unique n m k
  (H : forall q, (n | q) -> (m | q) -> (k | q))
  : (n | k) -> (m | k) -> nat_lcm n m = k.n, m, k: nat
H: forall q : nat, (n | q) -> (m | q) -> (k | q)
(n | k) -> (m | k) -> nat_lcm n m = k
Proof.n, m, k: nat
H: forall q : nat, (n | q) -> (m | q) -> (k | q)
(n | k) -> (m | k) -> nat_lcm n m = k
  intros H1 H2.n, m, k: nat
H: forall q : nat, (n | q) -> (m | q) -> (k | q)
H1: (n | k)
H2: (m | k)
nat_lcm n m = k
  rapply nat_divides_antisym.
Defined.

(** As a corollary of uniqueness, we get that the least common multiple operation is commutative. *)
Definition nat_lcm_comm n m : nat_lcm n m = nat_lcm m n.n, m: nat
nat_lcm n m = nat_lcm m n
Proof.n, m: nat
nat_lcm n m = nat_lcm m n
  rapply nat_lcm_unique.
Defined.

(** [nat_lcm] is associative. *)
Definition nat_lcm_assoc n m k : nat_lcm n (nat_lcm m k) = nat_lcm (nat_lcm n m) k.n, m, k: nat
nat_lcm n (nat_lcm m k) = nat_lcm (nat_lcm n m) k
Proof.n, m, k: nat
nat_lcm n (nat_lcm m k) = nat_lcm (nat_lcm n m) k
  rapply nat_lcm_unique.n, m, k: nat
forall q : nat,
(n | q) ->
(nat_lcm m k | q) -> (nat_lcm (nat_lcm n m) k | q)
  intros q H1 H2.n, m, k, q: nat
H1: (n | q)
H2: (nat_lcm m k | q)
(nat_lcm (nat_lcm n m) k | q)
  rapply nat_divides_l_lcm.n, m, k, q: nat
H1: (n | q)
H2: (nat_lcm m k | q)
(nat_lcm n m | q)
  rapply nat_divides_l_lcm.n, m, k, q: nat
H1: (n | q)
H2: (nat_lcm m k | q)
(m | q)
  rapply (nat_divides_trans _ H2).
Defined.

(** ** Prime Numbers *)

(** A prime number is a number greater than [1] that is only divisible by [1] and itself. *)
Class IsPrime (n : nat) : Type0 := {
  gt_one_isprime :: 1 < n;
  isprime : forall m, (m | n) -> (m = 1) + (m = n);
}.

Definition issig_IsPrime n : _ <~> IsPrime n := ltac:(issig).

Instance ishprop_isprime `{Funext} n : IsHProp (IsPrime n).H: Funext
n: nat
IsHProp (IsPrime n)
Proof.H: Funext
n: nat
IsHProp (IsPrime n)
  napply istrunc_equiv_istrunc.H: Funext
n: nat
?Goal <~> IsPrime n
H: Funext
n: nat
IsHProp ?Goal
  1: apply issig_IsPrime.H: Funext
n: nat
IsHProp
  {_ : 1 < n &
  forall m : nat, (m | n) -> (m = 1) + (m = n)}
  rapply istrunc_sigma.H: Funext
n: nat
1 < n ->
IsHProp (forall m : nat, (m | n) -> (m = 1) + (m = n))
  intros H1.H: Funext
n: nat
H1: 1 < n
IsHProp (forall m : nat, (m | n) -> (m = 1) + (m = n))
  snapply istrunc_forall.H: Funext
n: nat
H1: 1 < n
forall a : nat,
IsHProp
  ((fun a0 : nat => (a0 | n) -> (a0 = 1) + (a0 = n)) a)
  intros m.H: Funext
n: nat
H1: 1 < n
m: nat
IsHProp
  ((fun a : nat => (a | n) -> (a = 1) + (a = n)) m)
  snapply istrunc_forall.H: Funext
n: nat
H1: 1 < n
m: nat
forall a : (m | n),
IsHProp
  ((fun _ : (m | n) => ((m = 1) + (m = n))%type) a)
  intros d.H: Funext
n: nat
H1: 1 < n
m: nat
d: (m | n)
IsHProp
  ((fun _ : (m | n) => ((m = 1) + (m = n))%type) d)
  rapply ishprop_sum.H: Funext
n: nat
H1: 1 < n
m: nat
d: (m | n)
m = 1 -> m = n -> Empty
  intros p q.H: Funext
n: nat
H1: 1 < n
m: nat
d: (m | n)
p: m = 1
q: m = n
Empty
  napply (snd neq_iff_lt_or_gt _ (p^ @ q)).H: Funext
n: nat
H1: 1 < n
m: nat
d: (m | n)
p: m = 1
q: m = n
((1 < n) + (1 > n))%type
  by left.
Defined.

(** [0] is not a prime number. *)
Definition not_isprime_zero : ~ IsPrime 0.~ IsPrime 0
Proof.~ IsPrime 0
  intros H.H: IsPrime 0
Empty
  rapply not_lt_zero_r.
Defined.

(** [1] is not a prime number. *)
Definition not_isprime_one : ~ IsPrime 1.~ IsPrime 1
Proof.~ IsPrime 1
  intros H.H: IsPrime 1
Empty
  rapply (lt_irrefl 1).
Defined.

(** Being prime is a decidable property. We give an inefficient procedure for determining primality. More efficient procedures can be given, but for proofs this suffices. *)
Instance decidable_isprime@{} n : Decidable (IsPrime n).n: nat
Decidable (IsPrime n)
Proof.n: nat
Decidable (IsPrime n)
  (** First we begin by discarding the [n = 0] case as we can easily prove that [0] is not prime. *)
  destruct n.Decidable (IsPrime 0)
n: nat
Decidable (IsPrime n.+1)
  1: right; exact not_isprime_zero.n: nat
Decidable (IsPrime n.+1)
  (** Next, we rewrite [IsPrime n.+1] as the equivalent sigma type. *)
  napply decidable_equiv'.n: nat
?Goal <~> IsPrime n.+1
n: nat
Decidable ?Goal
  1: napply issig_IsPrime.n: nat
Decidable
  {_ : 1 < n.+1 &
  forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)}
  (** The condition in the first component in [IsPrime] is clearly decidable, so we can proceed to the second component. *)
  napply decidable_equiv'.n: nat
?Goal <~>
{_ : 1 < n.+1 &
forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)}
n: nat
Decidable ?Goal
  1: exact (equiv_sigma_prod0 _ _)^-1%equiv.n: nat
Decidable
  ((1 < n.+1) *
   (forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)))
  snapply decidable_prod.n: nat
Decidable (1 < n.+1)
n: nat
Decidable
  (forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1))
  1: exact _.n: nat
Decidable
  (forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1))
  (** In order to show that this [forall] is decidable, we will exhibit it as a [for_all] statement over a given list. The predicate will be the conclusion we wish to reach here, and the list will consist of all numbers with a condition equivalent to the divisibility condition. *)
  pose (P := fun m => ((m = 1) + (m = n.+1))%type : Type0).n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
Decidable
  (forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1))
  pose (l := list_filter (seq n.+2) (fun x => (x | n.+1)) _).n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
Decidable
  (forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1))
  rapply (decidable_iff (A := for_all P l)).n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
for_all P l <->
(forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1))
  split.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
for_all P l ->
forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)
n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
(forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)) ->
for_all P l
  -n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
for_all P l ->
forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1) intros Pl x d.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
Pl: for_all P l
x: nat
d: (x | n.+1)
((x = 1) + (x = n.+1))%type
    apply inlist_for_all with l x in Pl.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
x: nat
Pl: P x
d: (x | n.+1)
((x = 1) + (x = n.+1))%type
n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
Pl: for_all P l
x: nat
d: (x | n.+1)
InList x l
    1: exact Pl.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
Pl: for_all P l
x: nat
d: (x | n.+1)
InList x l
    apply inlist_filter.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
Pl: for_all P l
x: nat
d: (x | n.+1)
(InList x (seq n.+2) * (x | n.+1))%type
    split; only 2: assumption.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
Pl: for_all P l
x: nat
d: (x | n.+1)
InList x (seq n.+2)
    apply inlist_seq.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
Pl: for_all P l
x: nat
d: (x | n.+1)
x < n.+2
    apply leq_divides in d.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
Pl: for_all P l
x: nat
d: x <= n.+1
x < n.+2
n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
Pl: for_all P l
x: nat
d: (x | n.+1)
0 < n.+1
    1,2: exact _.
  -n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
(forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)) ->
for_all P l intros H.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
H: forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)
for_all P l
    apply for_all_inlist.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
H: forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)
forall x : nat, InList x l -> P x
    intros x H'.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
H: forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)
x: nat
H': InList x l
P x
    apply inlist_filter in H'.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
H: forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)
x: nat
H': (InList x (seq n.+2) * (x | n.+1))%type
P x
    destruct H' as [p H'].n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
H: forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)
x: nat
p: InList x (seq n.+2)
H': (x | n.+1)
P x
    apply inlist_seq in p.n: nat
P:= fun m : nat => (m = 1) + (m = n.+1) : Type0: nat -> Type0
l:= list_filter (seq n.+2) (fun x : nat => (x | n.+1))
  (fun x : nat => decidable_nat_divides x n.+1): list nat
H: forall m : nat, (m | n.+1) -> (m = 1) + (m = n.+1)
x: nat
p: x < n.+2
H': (x | n.+1)
P x
    rapply H.
Defined.

(** We can show that the first 8 primes are prime as expected. *)
Instance isprime_2 : IsPrime 2 := ltac:(decide).
Instance isprime_3 : IsPrime 3 := ltac:(decide).
Instance isprime_5 : IsPrime 5 := ltac:(decide).
Instance isprime_7 : IsPrime 7 := ltac:(decide).
Instance isprime_11 : IsPrime 11 := ltac:(decide).
Instance isprime_13 : IsPrime 13 := ltac:(decide).
Instance isprime_17 : IsPrime 17 := ltac:(decide).
Instance isprime_19 : IsPrime 19 := ltac:(decide).

(** Similarly, we can see that other natural numbers are not prime. *)
Definition not_isprime_0 : not (IsPrime 0) := ltac:(decide).
Definition not_isprime_1 : not (IsPrime 1) := ltac:(decide).
Definition not_isprime_4 : not (IsPrime 4) := ltac:(decide).

(** We can define the type of prime numbers as a subtype of natural numbers. *)
Definition Prime : Type0 := {n : nat & IsPrime n}.

Coercion nat_of_prime (p : Prime) : nat := p.1.
Instance isprime_prime (p : Prime) : IsPrime p := p.2.

Instance lt_zero_prime (p : Prime) : 0 < p
  := lt_trans _ gt_one_isprime.

(** A prime [p] is coprime to a natural number [n] iff [p] does not divide [n]. *)
Definition nat_coprime_iff_not_divides (p : Prime) n
  : nat_gcd p n = 1 <-> ~ (p | n).p: Prime
n: nat
nat_gcd p n = 1 <-> ~ (p | n)
Proof.p: Prime
n: nat
nat_gcd p n = 1 <-> ~ (p | n)
  split.p: Prime
n: nat
nat_gcd p n = 1 -> ~ (p | n)
p: Prime
n: nat
~ (p | n) -> nat_gcd p n = 1
  -p: Prime
n: nat
nat_gcd p n = 1 -> ~ (p | n) intros q [d r].p: Prime
n: nat
q: nat_gcd p n = 1
d: nat
r: d * p = n
Empty
    destruct r.p: Prime
d: nat
q: nat_gcd p (d * p) = 1
Empty
    rewrite (nat_gcd_r_add_r_mul p 0) in q.p: Prime
d: nat
q: nat_gcd p 0 = 1
Empty
    rewrite nat_gcd_zero_r in q.p: Prime
d: nat
q: p = 1
Empty
    apply (@neq_iff_lt_or_gt p 1).p: Prime
d: nat
q: p = 1
((p < 1) + (p > 1))%type
p: Prime
d: nat
q: p = 1
p = 1
    1: right; exact _.p: Prime
d: nat
q: p = 1
p = 1
    exact q.
  -p: Prime
n: nat
~ (p | n) -> nat_gcd p n = 1 intros nd.p: Prime
n: nat
nd: ~ (p | n)
nat_gcd p n = 1
    rapply nat_gcd_unique.p: Prime
n: nat
nd: ~ (p | n)
forall q : nat, (q | p) -> (q | n) -> (q | 1)
    intros q H1 H2.p: Prime
n: nat
nd: ~ (p | n)
q: nat
H1: (q | p)
H2: (q | n)
(q | 1)
    apply isprime in H1.p: Prime
n: nat
nd: ~ (p | n)
q: nat
H1: ((q = 1) + (q = p))%type
H2: (q | n)
(q | 1)
    destruct H1 as [H1|H1].p: Prime
n: nat
nd: ~ (p | n)
q: nat
H1: q = 1
H2: (q | n)
(q | 1)
p: Prime
n: nat
nd: ~ (p | n)
q: nat
H1: q = p
H2: (q | n)
(q | 1)
    +p: Prime
n: nat
nd: ~ (p | n)
q: nat
H1: q = 1
H2: (q | n)
(q | 1) destruct H1; exact _.
    +p: Prime
n: nat
nd: ~ (p | n)
q: nat
H1: q = p
H2: (q | n)
(q | 1) destruct H1; contradiction.
Defined.

(** When a prime number divides a multiple, then the prime must divide one of the factors. *)
Definition nat_divides_prime_l (p : Prime) n m
  : (p | n * m) -> (p | n) + (p | m).p: Prime
n, m: nat
(p | n * m) -> (p | n) + (p | m)
Proof.p: Prime
n, m: nat
(p | n * m) -> (p | n) + (p | m)
  intros d.p: Prime
n, m: nat
d: (p | n * m)
((p | n) + (p | m))%type
  destruct (dec (p | n)) as [H|H].p: Prime
n, m: nat
d: (p | n * m)
H: (p | n)
((p | n) + (p | m))%type
p: Prime
n, m: nat
d: (p | n * m)
H: ~ (p | n)
((p | n) + (p | m))%type
  1: by left.p: Prime
n, m: nat
d: (p | n * m)
H: ~ (p | n)
((p | n) + (p | m))%type
  right.p: Prime
n, m: nat
d: (p | n * m)
H: ~ (p | n)
(p | m)
  apply nat_coprime_iff_not_divides in H.p: Prime
n, m: nat
d: (p | n * m)
H: nat_gcd p n = 1
(p | m)
  destruct (nat_bezout_pos_l p n _) as [x [y q]].p: Prime
n, m: nat
d: (p | n * m)
H: nat_gcd p n = 1
x, y: nat
q: x * p = nat_gcd p n + y * n
(p | m)
  destruct H^; clear H.p: Prime
n, m: nat
d: (p | n * m)
x, y: nat
q: x * p = 1 + y * n
(p | m)
  destruct d as [d r].p: Prime
n, m, d: nat
r: d * p = n * m
x, y: nat
q: x * p = 1 + y * n
(p | m)
  exists (x * m - y * d).p: Prime
n, m, d: nat
r: d * p = n * m
x, y: nat
q: x * p = 1 + y * n
(x * m - y * d) * p = m
  lhs napply nat_dist_sub_r.p: Prime
n, m, d: nat
r: d * p = n * m
x, y: nat
q: x * p = 1 + y * n
x * m * p - y * d * p = m
  rewrite <- 2 nat_mul_assoc.p: Prime
n, m, d: nat
r: d * p = n * m
x, y: nat
q: x * p = 1 + y * n
x * (m * p) - y * (d * p) = m
  rewrite <- (nat_mul_comm p).p: Prime
n, m, d: nat
r: d * p = n * m
x, y: nat
q: x * p = 1 + y * n
x * (p * m) - y * (d * p) = m
  destruct r^; clear r.p: Prime
n, m, d, x, y: nat
q: x * p = 1 + y * n
x * (p * m) - y * (n * m) = m
  rewrite 2 nat_mul_assoc.p: Prime
n, m, d, x, y: nat
q: x * p = 1 + y * n
x * p * m - y * n * m = m
  lhs_V napply nat_dist_sub_r.p: Prime
n, m, d, x, y: nat
q: x * p = 1 + y * n
(x * p - y * n) * m = m
  rhs_V napply nat_mul_one_l.p: Prime
n, m, d, x, y: nat
q: x * p = 1 + y * n
(x * p - y * n) * m = 1 * m
  apply (ap (fun x => nat_mul x m)).p: Prime
n, m, d, x, y: nat
q: x * p = 1 + y * n
x * p - y * n = 1
  apply nat_moveR_nV.p: Prime
n, m, d, x, y: nat
q: x * p = 1 + y * n
x * p = 1 + y * n
  exact q.
Defined.

(** ** Composite Numbers *)

(** A natural number larger than [1] is composite if it has a divisor other than [1] and itself. *)
Class IsComposite n : Type0
  := iscomposite : exists a, 1 < a < n /\ (a | n).

Definition gt_1_iscomposite@{} n : IsComposite n -> 1 < n.n: nat
IsComposite n -> 1 < n
Proof.n: nat
IsComposite n -> 1 < n
  intros [a [[H1 H2] H3]].n, a: nat
H1: 1 < a
H2: a < n
H3: (a | n)
1 < n
  exact _.
Defined.
Hint Immediate gt_1_iscomposite : typeclass_instances.

(** Being composite is a decidable property. *)
Instance decidable_iscomposite@{} n : Decidable (IsComposite n).n: nat
Decidable (IsComposite n)
Proof.n: nat
Decidable (IsComposite n)
  unfold IsComposite.n: nat
Decidable {a : nat & ((1 < a < n) * (a | n))%type}
  rapply (decidable_exists_nat n).n: nat
forall k : nat, (1 < k < n) * (k | n) -> k < n
  intros k c.n, k: nat
c: ((1 < k < n) * (k | n))%type
k < n
  exact (snd (fst c)).
Defined.

(** For a number larger than [1], being prime is equivalent to not being composite. *)
Definition isprime_iff_not_iscomposite@{} n
  : IsPrime n <-> 1 < n /\ ~ IsComposite n.n: nat
IsPrime n <-> (1 < n) * ~ IsComposite n
Proof.n: nat
IsPrime n <-> (1 < n) * ~ IsComposite n
  split.n: nat
IsPrime n -> (1 < n) * ~ IsComposite n
n: nat
(1 < n) * ~ IsComposite n -> IsPrime n
  -n: nat
IsPrime n -> (1 < n) * ~ IsComposite n intros H.n: nat
H: IsPrime n
((1 < n) * ~ IsComposite n)%type
    split; only 1: exact _.n: nat
H: IsPrime n
~ IsComposite n
    intros [a [[H2 H3] H4]].n: nat
H: IsPrime n
a: nat
H2: 1 < a
H3: a < n
H4: (a | n)
Empty
    apply isprime in H4.n: nat
H: IsPrime n
a: nat
H2: 1 < a
H3: a < n
H4: ((a = 1) + (a = n))%type
Empty
    destruct H4 as [H4|H4]; destruct H4; exact (lt_irrefl _ _).
  -n: nat
(1 < n) * ~ IsComposite n -> IsPrime n intros [H1 H].n: nat
H1: 1 < n
H: ~ IsComposite n
IsPrime n
    rapply Build_IsPrime.n: nat
H1: 1 < n
H: ~ IsComposite n
forall m : nat, (m | n) -> (m = 1) + (m = n)
    intros m d.n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
((m = 1) + (m = n))%type
    destruct (dec (1 < d.1)) as [H2|H2].n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
((m = 1) + (m = n))%type
n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: ~ (1 < d.1)
((m = 1) + (m = n))%type
    +n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
((m = 1) + (m = n))%type pose proof (divides_divisor _ _ d) as d'.n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': (d.1 | n)
((m = 1) + (m = n))%type
      apply leq_divides in d'.n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': d.1 <= n
((m = 1) + (m = n))%type
n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': (d.1 | n)
0 < n
      2: exact _.n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': d.1 <= n
((m = 1) + (m = n))%type
      apply equiv_leq_lt_or_eq in d'.n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': ((d.1 < n) + (d.1 = n))%type
((m = 1) + (m = n))%type
      destruct d' as [d'|d'].n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': d.1 < n
((m = 1) + (m = n))%type
n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': d.1 = n
((m = 1) + (m = n))%type
      *n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': d.1 < n
((m = 1) + (m = n))%type assert (H' : IsComposite n).n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': d.1 < n
IsComposite n
n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': d.1 < n
H': IsComposite n
((m = 1) + (m = n))%type
        {n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': d.1 < n
IsComposite n exists d.1.n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': d.1 < n
((1 < d.1 < n) * (d.1 | n))%type
          split; only 1: split; exact _. }n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': d.1 < n
H': IsComposite n
((m = 1) + (m = n))%type
          contradiction H.
      *n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 < d.1
d': d.1 = n
((m = 1) + (m = n))%type destruct d as [d r].n: nat
H1: 1 < n
H: ~ IsComposite n
m, d: nat
r: d * m = n
H2: 1 < (d; r).1
d': (d; r).1 = n
((m = 1) + (m = n))%type
        simpl in *.n: nat
H1: 1 < n
H: ~ IsComposite n
m, d: nat
r: d * m = n
H2: 1 < d
d': d = n
((m = 1) + (m = n))%type
        destruct d'.d, m: nat
r: d * m = d
H1: 1 < d
H: ~ IsComposite d
H2: 1 < d
((m = 1) + (m = d))%type
         left.d, m: nat
r: d * m = d
H1: 1 < d
H: ~ IsComposite d
H2: 1 < d
m = 1
         rewrite <- nat_div_cancel with d.d, m: nat
r: d * m = d
H1: 1 < d
H: ~ IsComposite d
H2: 1 < d
m = d / d
d, m: nat
r: d * m = d
H1: 1 < d
H: ~ IsComposite d
H2: 1 < d
0 < d
         2: exact _.d, m: nat
r: d * m = d
H1: 1 < d
H: ~ IsComposite d
H2: 1 < d
m = d / d
         rewrite <- nat_div_mul_cancel_l with d m.d, m: nat
r: d * m = d
H1: 1 < d
H: ~ IsComposite d
H2: 1 < d
(d * m) / d = d / d
d, m: nat
r: d * m = d
H1: 1 < d
H: ~ IsComposite d
H2: 1 < d
0 < d
         2: exact _.d, m: nat
r: d * m = d
H1: 1 < d
H: ~ IsComposite d
H2: 1 < d
(d * m) / d = d / d
         by apply (ap (fun x => x / d)).
    +n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: ~ (1 < d.1)
((m = 1) + (m = n))%type apply geq_iff_not_lt in H2.n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
d: (m | n)
H2: 1 >= d.1
((m = 1) + (m = n))%type
      destruct d as [d r].n: nat
H1: 1 < n
H: ~ IsComposite n
m, d: nat
r: d * m = n
H2: 1 >= (d; r).1
((m = 1) + (m = n))%type
      simpl in *; hnf in H2.n: nat
H1: 1 < n
H: ~ IsComposite n
m, d: nat
r: d * m = n
H2: d <= 1
((m = 1) + (m = n))%type
      destruct d.n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
r: 0 * m = n
H2: 0 <= 1
((m = 1) + (m = n))%type
n: nat
H1: 1 < n
H: ~ IsComposite n
m, d: nat
r: d.+1 * m = n
H2: d.+1 <= 1
((m = 1) + (m = n))%type
      {n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
r: 0 * m = n
H2: 0 <= 1
((m = 1) + (m = n))%type rewrite nat_mul_zero_l in r.n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
r: 0 = n
H2: 0 <= 1
((m = 1) + (m = n))%type
        destruct n.H1: 1 < 0
H: ~ IsComposite 0
m: nat
r: 0 = 0
H2: 0 <= 1
((m = 1) + (m = 0))%type
n: nat
H1: 1 < n.+1
H: ~ IsComposite n.+1
m: nat
r: 0 = n.+1
H2: 0 <= 1
((m = 1) + (m = n.+1))%type
        1: contradiction (not_lt_zero_r _ H1).n: nat
H1: 1 < n.+1
H: ~ IsComposite n.+1
m: nat
r: 0 = n.+1
H2: 0 <= 1
((m = 1) + (m = n.+1))%type
        contradiction (neq_nat_zero_succ _ r). }n: nat
H1: 1 < n
H: ~ IsComposite n
m, d: nat
r: d.+1 * m = n
H2: d.+1 <= 1
((m = 1) + (m = n))%type
      destruct d.n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
r: 1 * m = n
H2: 1 <= 1
((m = 1) + (m = n))%type
n: nat
H1: 1 < n
H: ~ IsComposite n
m, d: nat
r: d.+2 * m = n
H2: d.+2 <= 1
((m = 1) + (m = n))%type
      {n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
r: 1 * m = n
H2: 1 <= 1
((m = 1) + (m = n))%type rewrite nat_mul_one_l in r.n: nat
H1: 1 < n
H: ~ IsComposite n
m: nat
r: m = n
H2: 1 <= 1
((m = 1) + (m = n))%type
        by right. }n: nat
H1: 1 < n
H: ~ IsComposite n
m, d: nat
r: d.+2 * m = n
H2: d.+2 <= 1
((m = 1) + (m = n))%type
      apply leq_pred' in H2.n: nat
H1: 1 < n
H: ~ IsComposite n
m, d: nat
r: d.+2 * m = n
H2: d.+1 <= 0
((m = 1) + (m = n))%type
      contradiction (not_lt_zero_r d).
Defined.

(** And since [IsComposite] is decidable, we can show that being not prime is equivalent to being composite. *)
Definition not_isprime_iff_iscomposite@{} n
  : 1 < n /\ ~ IsPrime n <-> IsComposite n.n: nat
(1 < n) * ~ IsPrime n <-> IsComposite n
Proof.n: nat
(1 < n) * ~ IsPrime n <-> IsComposite n
  napply iff_compose.n: nat
(1 < n) * ~ IsPrime n <-> ?Goal
n: nat
?Goal <-> IsComposite n
  -n: nat
(1 < n) * ~ IsPrime n <-> ?Goal napply iff_functor_prod.n: nat
1 < n <-> ?Goal0
n: nat
~ IsPrime n <-> ?Goal1
    1: exact iff_refl.n: nat
~ IsPrime n <-> ?Goal0
    napply iff_compose.n: nat
~ IsPrime n <-> ?Goal1
n: nat
?Goal1 <-> ?Goal0
    +n: nat
~ IsPrime n <-> ?Goal1 apply iff_not.n: nat
IsPrime n <-> ?B
      rapply isprime_iff_not_iscomposite.
    +n: nat
~ ((1 < n) * ~ IsComposite n) <-> ?Goal0 rapply iff_not_prod.
  -n: nat
(1 < n) * (~ (1 < n) + ~~ IsComposite n) <->
IsComposite n napply iff_compose.n: nat
(1 < n) * (~ (1 < n) + ~~ IsComposite n) <-> ?Goal
n: nat
?Goal <-> IsComposite n
    1: napply sum_distrib_l.n: nat
(1 < n) * ~ (1 < n) + (1 < n) * ~~ IsComposite n <->
IsComposite n
    napply iff_compose.n: nat
(1 < n) * ~ (1 < n) + (1 < n) * ~~ IsComposite n <->
?Goal
n: nat
?Goal <-> IsComposite n
    +n: nat
(1 < n) * ~ (1 < n) + (1 < n) * ~~ IsComposite n <->
?Goal napply iff_functor_sum.n: nat
(1 < n) * ~ (1 < n) <-> ?Goal0
n: nat
(1 < n) * ~~ IsComposite n <-> ?Goal1
      1: apply iff_contradiction.n: nat
(1 < n) * ~~ IsComposite n <-> ?Goal0
      napply iff_functor_prod.n: nat
1 < n <-> ?Goal0
n: nat
~~ IsComposite n <-> ?Goal1
      1: exact iff_refl.n: nat
~~ IsComposite n <-> ?Goal0
      rapply iff_stable.
    +n: nat
Empty + (1 < n) * IsComposite n <-> IsComposite n napply iff_compose.n: nat
Empty + (1 < n) * IsComposite n <-> ?Goal
n: nat
?Goal <-> IsComposite n
      1: rapply sum_empty_l.n: nat
(1 < n) * IsComposite n <-> IsComposite n
      split; only 1: exact snd.n: nat
IsComposite n -> (1 < n) * IsComposite n
      intros H; split; only 2: exact H.n: nat
H: IsComposite n
1 < n
      exact _.
Defined.

(** ** Fundamental theorem of arithmetic *)

(** Every natural number greater than [1] has a prime divisor. *)
Definition exists_prime_divisor@{} n
  : 1 < n -> exists (p : Prime), (p | n).n: nat
1 < n -> {p : Prime & (p | n)}
Proof.n: nat
1 < n -> {p : Prime & (p | n)}
  revert n; snapply nat_ind_strong; hnf; intros n IHn H.n: nat
IHn: forall m : nat, m < n -> 1 < m -> {p : Prime & (p | m)}
H: 1 < n
{p : Prime & (p | n)}
  destruct (dec (IsPrime n)) as [x|x].n: nat
IHn: forall m : nat, m < n -> 1 < m -> {p : Prime & (p | m)}
H: 1 < n
x: IsPrime n
{p : Prime & (p | n)}
n: nat
IHn: forall m : nat, m < n -> 1 < m -> {p : Prime & (p | m)}
H: 1 < n
x: ~ IsPrime n
{p : Prime & (p | n)}
  1: exists (_; x); exact _.n: nat
IHn: forall m : nat, m < n -> 1 < m -> {p : Prime & (p | m)}
H: 1 < n
x: ~ IsPrime n
{p : Prime & (p | n)}
  pose (r := (H, x)).n: nat
IHn: forall m : nat, m < n -> 1 < m -> {p : Prime & (p | m)}
H: 1 < n
x: ~ IsPrime n
r:= (H, x): ((1 < n) * ~ IsPrime n)%type
{p : Prime & (p | n)}
  apply not_isprime_iff_iscomposite in r.n: nat
IHn: forall m : nat, m < n -> 1 < m -> {p : Prime & (p | m)}
H: 1 < n
x: ~ IsPrime n
r: IsComposite n
{p : Prime & (p | n)}
  destruct r as [d [[H1 H2] H3]].n: nat
IHn: forall m : nat, m < n -> 1 < m -> {p : Prime & (p | m)}
H: 1 < n
x: ~ IsPrime n
d: nat
H1: 1 < d
H2: d < n
H3: (d | n)
{p : Prime & (p | n)}
  destruct (IHn d _ _) as [p r].n: nat
IHn: forall m : nat, m < n -> 1 < m -> {p : Prime & (p | m)}
H: 1 < n
x: ~ IsPrime n
d: nat
H1: 1 < d
H2: d < n
H3: (d | n)
p: Prime
r: (p | d)
{p : Prime & (p | n)}
  exists p.n: nat
IHn: forall m : nat, m < n -> 1 < m -> {p : Prime & (p | m)}
H: 1 < n
x: ~ IsPrime n
d: nat
H1: 1 < d
H2: d < n
H3: (d | n)
p: Prime
r: (p | d)
(p | n)
  exact _.
Defined.

(** Any natural number can either be written as a product of primes or is zero. *)
Definition prime_factorization@{} n
  : 0 < n
    -> exists (l : list Prime),
      n = fold_right (fun (p : Prime) n => nat_mul p n) 1 l.n: nat
0 < n ->
{l : list Prime &
n =
fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
Proof.n: nat
0 < n ->
{l : list Prime &
n =
fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
  revert n; snapply nat_ind_strong; hnf; intros n IHn H.n: nat
IHn: forall m : nat,
m < n ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
H: 0 < n
{l : list Prime &
n =
fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
  destruct H as [|n IH].IHn: forall m : nat,
m < 1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
{l : list Prime &
1 =
fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
{l : list Prime &
n.+1 =
fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
  1: exists nil; reflexivity.n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
{l : list Prime &
n.+1 =
fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
  destruct (exists_prime_divisor n.+1 _) as [p d].n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
p: Prime
d: (p | n.+1)
{l : list Prime &
n.+1 =
fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
  pose proof (l := lt_divides d.1 n.+1 _ _ _).n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
p: Prime
d: (p | n.+1)
l: d.1 < n.+1
{l : list Prime &
n.+1 =
fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
  destruct d as [k H].n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
p: Prime
k: nat
H: k * p = n.+1
l: (k; H).1 < n.+1
{l : list Prime &
n.+1 =
fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
  destruct (IHn k l) as [f r].n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
p: Prime
k: nat
H: k * p = n.+1
l: (k; H).1 < n.+1
0 < k
n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
p: Prime
k: nat
H: k * p = n.+1
l: (k; H).1 < n.+1
f: list Prime
r: k =
fold_right (fun (p : Prime) (n : nat) => p * n) 1
  f
{l : list Prime &
n.+1 =
fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
  {n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
p: Prime
k: nat
H: k * p = n.+1
l: (k; H).1 < n.+1
0 < k destruct H, k.n: nat
p: Prime
IHn: forall m : nat,
m < 0 * p ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
l: (0; 1).1 < 0 * p
0 < 0
n: nat
p: Prime
k: nat
IHn: forall m : nat,
m < k.+1 * p ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
l: (k.+1; 1).1 < k.+1 * p
0 < k.+1
    1: contradiction (lt_irrefl 0).n: nat
p: Prime
k: nat
IHn: forall m : nat,
m < k.+1 * p ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
l: (k.+1; 1).1 < k.+1 * p
0 < k.+1
    exact _. }n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
p: Prime
k: nat
H: k * p = n.+1
l: (k; H).1 < n.+1
f: list Prime
r: k =
fold_right (fun (p : Prime) (n : nat) => p * n) 1
  f
{l : list Prime &
n.+1 =
fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
  exists (p :: f)%list.n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
p: Prime
k: nat
H: k * p = n.+1
l: (k; H).1 < n.+1
f: list Prime
r: k =
fold_right (fun (p : Prime) (n : nat) => p * n) 1
  f
n.+1 =
fold_right (fun (p : Prime) (n : nat) => p * n) 1
  (p :: f)
  simpl; destruct r.n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
p: Prime
k: nat
H: k * p = n.+1
l: (k; H).1 < n.+1
f: list Prime
n.+1 = p * k
  symmetry.n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
p: Prime
k: nat
H: k * p = n.+1
l: (k; H).1 < n.+1
f: list Prime
p * k = n.+1
  lhs napply nat_mul_comm.n: nat
IHn: forall m : nat,
m < n.+1 ->
0 < m ->
{l : list Prime & m = fold_right (fun (p : Prime) (n : nat) => p * n) 1 l}
IH: 1 <= n
p: Prime
k: nat
H: k * p = n.+1
l: (k; H).1 < n.+1
f: list Prime
k * p = n.+1
  exact H.
Defined.

(** TODO: show that any two prime factorizations are unique up to permutation of the lists. *)