Library HoTT.Spaces.Nat.Division
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.
Local Set Universe Minimization ToSet.
Local Open Scope nat_scope.
Basics.PathGroupoids Basics.Equivalences Types.Sigma Spaces.Nat.Core
Basics.Decidable Basics.Iff Types.Prod List.Theory Types.Sum Types.Arrow.
Local Set Universe Minimization ToSet.
Local Open Scope nat_scope.
Division of natural numbers
Divisibility
Class NatDivides (n m : nat) : Type0 := nat_divides : {k : nat & k × n = m}.
Notation "( n | m )" := (NatDivides n m) : nat_scope.
Notation "( n | m )" := (NatDivides n m) : nat_scope.
Any number divides 0.
1 divides any number.
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.
:= (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).
Proof.
intros [x p] [y q].
∃ (y × x).
lhs_V napply nat_mul_assoc.
lhs napply (ap _ p).
exact q.
Defined.
Hint Immediate nat_divides_trans : typeclass_instances.
Instance transitive_nat_divides : Transitive NatDivides := @nat_divides_trans.
Proof.
intros [x p] [y q].
∃ (y × x).
lhs_V napply nat_mul_assoc.
lhs napply (ap _ p).
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.
A right factor divides a product.
Divisibility of the product is implied by divisibility of the left factor.
Divisibility of the product is implied by divisibility of the right factor.
Multiplication is monotone with respect to divisibility.
Instance nat_divides_mul_monotone n m l p
: (n | m) → (l | p) → (n × l | m × p).
Proof.
intros [x r] [y q].
∃ (x × y).
destruct r, q.
lhs napply nat_mul_assoc.
rhs napply nat_mul_assoc.
napply (ap (fun x ⇒ nat_mul x _)).
lhs_V napply nat_mul_assoc.
rhs_V napply nat_mul_assoc.
napply ap.
apply nat_mul_comm.
Defined.
: (n | m) → (l | p) → (n × l | m × p).
Proof.
intros [x r] [y q].
∃ (x × y).
destruct r, q.
lhs napply nat_mul_assoc.
rhs napply nat_mul_assoc.
napply (ap (fun x ⇒ nat_mul x _)).
lhs_V napply nat_mul_assoc.
rhs_V napply nat_mul_assoc.
napply ap.
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).
Proof.
intros [x p] [y q].
∃ (x + y).
destruct p, q.
napply nat_dist_r.
Defined.
Proof.
intros [x p] [y q].
∃ (x + y).
destruct p, q.
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).
Proof.
intros [x p] [y q].
∃ (y - x).
lhs napply nat_dist_sub_r.
apply nat_moveR_nV.
lhs exact q.
lhs napply nat_add_comm.
exact (ap _ p^).
Defined.
Proof.
intros [x p] [y q].
∃ (y - x).
lhs napply nat_dist_sub_r.
apply nat_moveR_nV.
lhs exact q.
lhs napply nat_add_comm.
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).
Proof.
rewrite nat_add_comm; apply nat_divides_add_r.
Defined.
Proof.
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).
Proof.
intros [x p] [y q].
∃ (x - y).
destruct p, q.
napply nat_dist_sub_r.
Defined.
Proof.
intros [x p] [y q].
∃ (x - y).
destruct p, q.
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.
Proof.
destruct d as [d H].
destruct H.
destruct (nat_zero_or_gt_zero n) as [z | s].
2: exact s.
(* The remaining case is impossible. *)
destruct z; cbn in gt0.
rewrite nat_mul_zero_r in gt0.
exact gt0.
Defined.
: 0 < n.
Proof.
destruct d as [d H].
destruct H.
destruct (nat_zero_or_gt_zero n) as [z | s].
2: exact s.
(* The remaining case is impossible. *)
destruct z; cbn in gt0.
rewrite nat_mul_zero_r in gt0.
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.
Proof.
intros H1 [x p].
destruct p, x.
1: contradiction (not_lt_zero_r _ H1).
rapply (leq_mul_l _ _ 0).
Defined.
Proof.
intros H1 [x p].
destruct p, x.
1: contradiction (not_lt_zero_r _ H1).
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.
Proof.
rewrite <- d.2.
snapply (lt_leq_lt_trans (m:=1×n)).
1: rapply (leq_mul_l _ _ 0).
srapply (nat_mul_r_strictly_monotone (l:=0)).
rapply (gt_zero_divides n m).
Defined.
: n < m.
Proof.
rewrite <- d.2.
snapply (lt_leq_lt_trans (m:=1×n)).
1: rapply (leq_mul_l _ _ 0).
srapply (nat_mul_r_strictly_monotone (l:=0)).
rapply (gt_zero_divides n m).
Defined.
Divisibility is antisymmetric
Definition nat_divides_antisym n m : (n | m) → (m | n) → n = m.
Proof.
intros H1 H2.
destruct m; only 1: exact (H2.2^ @ nat_mul_zero_r _).
destruct n; only 1: exact ((nat_mul_zero_r _)^ @ H1.2).
snapply leq_antisym; napply leq_divides; exact _.
Defined.
Instance antisymmetric_divides : AntiSymmetric NatDivides
:= nat_divides_antisym.
Proof.
intros H1 H2.
destruct m; only 1: exact (H2.2^ @ nat_mul_zero_r _).
destruct n; only 1: exact ((nat_mul_zero_r _)^ @ H1.2).
snapply leq_antisym; napply leq_divides; exact _.
Defined.
Instance antisymmetric_divides : AntiSymmetric NatDivides
:= nat_divides_antisym.
Instance divides_divisor n m (H : (n | m)) : (H.1 | m).
Proof.
∃ n.
lhs napply nat_mul_comm.
exact H.2.
Defined.
Proof.
∃ n.
lhs napply nat_mul_comm.
exact H.2.
Defined.
Local Definition nat_div_mod_unique_helper b q1 q2 r1 r2
: r1 < b → r2 < b → q1 < q2 → b × q1 + r1 ≠ b × q2 + r2.
Proof.
intros H1 H2 H3 p.
rewrite 2 (nat_add_comm (b × _)) in p.
apply nat_moveL_nV in p.
rewrite nat_sub_l_add_r in p; only 2: rapply nat_mul_l_monotone.
rewrite <- nat_dist_sub_l in p.
rewrite nat_add_comm in p.
apply nat_moveR_nV in p.
napply (snd (@leq_iff_not_gt b (r1 - r2))).
2: exact (lt_leq_lt_trans _ H1).
rewrite p.
snapply (leq_mul_r _ _ 0).
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.
Proof.
intros H1 H2 p.
destruct (nat_trichotomy q1 q2) as [[q | q] | q].
- contradiction (nat_div_mod_unique_helper d q1 q2 r1 r2).
- split; trivial.
destruct q.
by apply isinj_nat_add_l in p.
- by contradiction (nat_div_mod_unique_helper d q2 q1 r2 r1).
Defined.
: r1 < d → r2 < d → d × q1 + r1 = d × q2 + r2
→ q1 = q2 ∧ r1 = r2.
Proof.
intros H1 H2 p.
destruct (nat_trichotomy q1 q2) as [[q | q] | q].
- contradiction (nat_div_mod_unique_helper d q1 q2 r1 r2).
- split; trivial.
destruct q.
by apply isinj_nat_add_l in p.
- 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).
Proof.
intros H.
apply hprop_allpath.
intros [x p] [y q].
rapply path_sigma_hprop.
destruct H as [|n]; simpl.
1: exact ((nat_mul_one_r _)^ @ p @ q^ @ nat_mul_one_r _).
refine (fst (nat_div_mod_unique n.+1 x y 0 0 _ _ _)).
lhs napply nat_add_zero_r.
rhs napply nat_add_zero_r.
rewrite 2 (nat_mul_comm n.+1).
exact (p @ q^).
Defined.
Proof.
intros H.
apply hprop_allpath.
intros [x p] [y q].
rapply path_sigma_hprop.
destruct H as [|n]; simpl.
1: exact ((nat_mul_one_r _)^ @ p @ q^ @ nat_mul_one_r _).
refine (fst (nat_div_mod_unique n.+1 x y 0 0 _ _ _)).
lhs napply nat_add_zero_r.
rhs napply nat_add_zero_r.
rewrite 2 (nat_mul_comm n.+1).
exact (p @ q^).
Defined.
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.
Proof.
intros d r.
induction x as [|x IHx] in y, q, u, H, d, r |- *; only 1: by split.
destruct u as [|u].
- destruct (IHx y q.+1 y _) as [p H'].
split; trivial.
rewrite <- p, nat_sub_zero_r, nat_sub_cancel, nat_add_zero_r.
simpl.
by rewrite nat_add_succ_r, <- 2 nat_add_assoc, nat_mul_succ_r.
- destruct (IHx y q u _) as [p H'].
split; trivial.
rewrite <- p, 2 nat_add_succ_l, <- nat_add_succ_r.
snapply ap.
rewrite nat_sub_succ_r.
apply nat_succ_pred.
rapply lt_moveL_nV.
Defined.
: let (q', u') := nat_div_mod x y q u in
x + y.+1 × q + (y - u) = y.+1 × q' + (y - u') ∧ u' ≤ y.
Proof.
intros d r.
induction x as [|x IHx] in y, q, u, H, d, r |- *; only 1: by split.
destruct u as [|u].
- destruct (IHx y q.+1 y _) as [p H'].
split; trivial.
rewrite <- p, nat_sub_zero_r, nat_sub_cancel, nat_add_zero_r.
simpl.
by rewrite nat_add_succ_r, <- 2 nat_add_assoc, nat_mul_succ_r.
- destruct (IHx y q u _) as [p H'].
split; trivial.
rewrite <- p, 2 nat_add_succ_l, <- nat_add_succ_r.
snapply ap.
rewrite nat_sub_succ_r.
apply nat_succ_pred.
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.
Proof.
destruct y as [|y]; only 1: reflexivity.
pose proof (p := fst (nat_div_mod_helper_spec x y 0 y _)).
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.
Proof.
apply nat_moveR_nV.
rhs napply nat_add_comm.
apply nat_div_mod_spec.
Defined.
Definition nat_div_mod_spec'' x y : x - x mod y = y × (x / y).
Proof.
apply nat_moveR_nV.
apply nat_div_mod_spec.
Defined.
Definition nat_mod_lt_r' n m r : r < m → n mod m < m.
Proof.
intros H; destruct H; only 1: exact _.
rapply (lt_leq_lt_trans (m:=m)).
Defined.
Hint Immediate nat_mod_lt_r' : typeclass_instances.
Proof.
destruct y as [|y]; only 1: reflexivity.
pose proof (p := fst (nat_div_mod_helper_spec x y 0 y _)).
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.
Proof.
apply nat_moveR_nV.
rhs napply nat_add_comm.
apply nat_div_mod_spec.
Defined.
Definition nat_div_mod_spec'' x y : x - x mod y = y × (x / y).
Proof.
apply nat_moveR_nV.
apply nat_div_mod_spec.
Defined.
Definition nat_mod_lt_r' n m r : r < m → n mod m < m.
Proof.
intros H; destruct H; only 1: exact _.
rapply (lt_leq_lt_trans (m:=m)).
Defined.
Hint Immediate nat_mod_lt_r' : typeclass_instances.
Instance nat_mod_leq_l n m : n mod m ≤ n.
Proof.
rewrite <- nat_div_mod_spec'.
rapply leq_moveR_nV.
Defined.
Proof.
rewrite <- nat_div_mod_spec'.
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)^).
:= 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)^).
:= 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.
n divided by 0 is 0 by convention.
n divided by 1 is n.
Definition nat_div_one_r n : n / 1 = n.
Proof.
lhs_V napply nat_mul_one_l.
lhs_V napply nat_add_zero_r.
symmetry; apply nat_div_mod_spec.
Defined.
Proof.
lhs_V napply nat_mul_one_l.
lhs_V napply nat_add_zero_r.
symmetry; apply nat_div_mod_spec.
Defined.
n divided by n is 1.
Definition nat_div_cancel n : 0 < n → n / n = 1.
Proof.
intros [|m _]; trivial.
napply (nat_div_unique _ _ _ 0); only 1: exact _.
lhs napply nat_add_zero_r.
napply nat_mul_one_r.
Defined.
Proof.
intros [|m _]; trivial.
napply (nat_div_unique _ _ _ 0); only 1: exact _.
lhs napply nat_add_zero_r.
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.
Proof.
intros H.
snapply (nat_div_unique _ _ _ _ H).
by rewrite nat_mul_zero_r, nat_add_zero_l.
Defined.
Proof.
intros H.
snapply (nat_div_unique _ _ _ _ H).
by rewrite nat_mul_zero_r, nat_add_zero_l.
Defined.
Definition nat_div_mul_cancel_l n m : 0 < n → (n × m) / n = m.
Proof.
intros H.
napply (nat_div_unique _ _ _ _ H).
apply nat_add_zero_r.
Defined.
Proof.
intros H.
napply (nat_div_unique _ _ _ _ H).
apply nat_add_zero_r.
Defined.
Definition nat_div_mul_cancel_r n m : 0 < m → (n × m) / m = n.
Proof.
rewrite nat_mul_comm.
apply nat_div_mul_cancel_l.
Defined.
Proof.
rewrite nat_mul_comm.
apply nat_div_mul_cancel_l.
Defined.
Definition nat_div_mul_add_cancel_l n m k : 0 < n → (n × m + k) / n = m + k / n.
Proof.
intros H.
rapply (nat_div_unique _ _ _ (k mod n) _).
rewrite nat_dist_l.
lhs_V napply nat_add_assoc.
f_ap.
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.
Proof.
rewrite nat_mul_comm.
apply nat_div_mul_add_cancel_l.
Defined.
Proof.
intros H.
rapply (nat_div_unique _ _ _ (k mod n) _).
rewrite nat_dist_l.
lhs_V napply nat_add_assoc.
f_ap.
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.
Proof.
rewrite nat_mul_comm.
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).
Proof.
intros kp m n p.
lhs_V rapply (nat_div_mul_cancel_l k).
rhs_V rapply (nat_div_mul_cancel_l k).
exact (ap (fun x ⇒ x / k) p).
Defined.
Proof.
intros kp m n p.
lhs_V rapply (nat_div_mul_cancel_l k).
rhs_V rapply (nat_div_mul_cancel_l 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).
Proof.
intros kp m n p.
lhs_V rapply (nat_div_mul_cancel_r _ k).
rhs_V rapply (nat_div_mul_cancel_r _ k).
exact (ap (fun x ⇒ x / k) p).
Defined.
Proof.
intros kp m n p.
lhs_V rapply (nat_div_mul_cancel_r _ k).
rhs_V rapply (nat_div_mul_cancel_r _ 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.
Proof.
destruct d.
1: reflexivity.
intros [x []].
rewrite nat_div_mul_cancel_r. 2: exact _.
rapply nat_div_mul_add_cancel_r.
Defined.
Definition nat_div_dist' n m d
: (d | m) → (n + m) / d = n / d + m / d.
Proof.
intros H.
rewrite (nat_add_comm n m).
rhs_V napply nat_add_comm.
rapply nat_div_dist.
Defined.
: (d | n) → (n + m) / d = n / d + m / d.
Proof.
destruct d.
1: reflexivity.
intros [x []].
rewrite nat_div_mul_cancel_r. 2: exact _.
rapply nat_div_mul_add_cancel_r.
Defined.
Definition nat_div_dist' n m d
: (d | m) → (n + m) / d = n / d + m / d.
Proof.
intros H.
rewrite (nat_add_comm n m).
rhs_V napply nat_add_comm.
rapply nat_div_dist.
Defined.
Definition nat_leq_mul_div_l n m
: n × (m / n) ≤ m.
Proof.
set (tmp := n × (m / n));
rewrite (nat_div_mod_spec m n);
unfold tmp; clear tmp.
exact _.
Defined.
: n × (m / n) ≤ m.
Proof.
set (tmp := n × (m / n));
rewrite (nat_div_mod_spec m n);
unfold tmp; clear tmp.
exact _.
Defined.
When n divides m, they are equal.
Definition nat_mul_div_cancel_r n m
: (n | m) → (m / n) × n = m.
Proof.
destruct n.
{ intros [k []]. cbn. symmetry; apply nat_mul_zero_r. }
intros [k []].
f_ap.
rapply nat_div_mul_cancel_r.
Defined.
Definition nat_mul_div_cancel_l n m
: (n | m) → n × (m / n) = m.
Proof.
rewrite nat_mul_comm.
apply nat_mul_div_cancel_r.
Defined.
: (n | m) → (m / n) × n = m.
Proof.
destruct n.
{ intros [k []]. cbn. symmetry; apply nat_mul_zero_r. }
intros [k []].
f_ap.
rapply nat_div_mul_cancel_r.
Defined.
Definition nat_mul_div_cancel_l n m
: (n | m) → n × (m / n) = m.
Proof.
rewrite nat_mul_comm.
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.
Proof.
intros lk nm km.
apply gt_iff_not_leq.
intro mknk.
apply (@gt_iff_not_leq m n); only 1: exact nm.
rewrite <- (nat_mul_div_cancel_l k m km).
napply (leq_trans (y:=k × (n / k))).
- rapply nat_mul_l_monotone.
- apply nat_leq_mul_div_l.
Defined.
: l < k → n < m → (k | m) → n / k < m / k.
Proof.
intros lk nm km.
apply gt_iff_not_leq.
intro mknk.
apply (@gt_iff_not_leq m n); only 1: exact nm.
rewrite <- (nat_mul_div_cancel_l k m km).
napply (leq_trans (y:=k × (n / k))).
- rapply nat_mul_l_monotone.
- apply nat_leq_mul_div_l.
Defined.
0 modulo n is 0.
Definition nat_mod_zero_l n : 0 mod n = 0.
Proof.
induction n; trivial.
apply nat_sub_cancel.
Defined.
Proof.
induction n; trivial.
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.
Proof.
intros H.
lhs_V napply nat_div_mod_spec'.
rewrite nat_div_lt.
- rewrite nat_mul_zero_r.
apply nat_sub_zero_r.
- exact H.
Defined.
Definition nat_mod_lt n k : k < n → k mod n = k.
Proof.
intros H.
lhs_V napply nat_div_mod_spec'.
rewrite nat_div_lt.
- rewrite nat_mul_zero_r.
apply nat_sub_zero_r.
- exact H.
Defined.
n modulo 1 is 0.
Definition nat_mod_divides n m : (m | n) → n mod m = 0.
Proof.
intros [x p].
destruct p.
destruct m.
{ simpl. apply nat_mul_zero_r. }
lhs_V napply nat_div_mod_spec'.
rewrite nat_div_mul_cancel_r; only 2: exact _.
apply nat_moveR_nV, nat_mul_comm.
Defined.
Proof.
intros [x p].
destruct p.
destruct m.
{ simpl. apply nat_mul_zero_r. }
lhs_V napply nat_div_mod_spec'.
rewrite nat_div_mul_cancel_r; only 2: exact _.
apply nat_moveR_nV, nat_mul_comm.
Defined.
Definition nat_mod_iff_divides n m : n mod m = 0 ↔ (m | n) .
Proof.
split.
2: exact (nat_mod_divides _ _).
intros p.
∃ (n / m).
rewrite nat_mul_comm.
lhs_V napply nat_add_zero_r.
rewrite <- p.
symmetry.
napply nat_div_mod_spec.
Defined.
Proof.
split.
2: exact (nat_mod_divides _ _).
intros p.
∃ (n / m).
rewrite nat_mul_comm.
lhs_V napply nat_add_zero_r.
rewrite <- p.
symmetry.
napply nat_div_mod_spec.
Defined.
Divisibility is therefore decidable.
Instance decidable_nat_divides n m : Decidable (n | m).
Proof.
napply decidable_iff.
1: apply nat_mod_iff_divides.
exact _.
Defined.
Proof.
napply decidable_iff.
1: apply nat_mod_iff_divides.
exact _.
Defined.
n modulo n is 0.
Definition nat_mod_cancel n : n mod n = 0.
Proof.
destruct n; trivial.
snapply (nat_mod_unique _ _ 1); only 1: exact _.
lhs napply nat_add_zero_r.
napply nat_mul_one_r.
Defined.
Proof.
destruct n; trivial.
snapply (nat_mod_unique _ _ 1); only 1: exact _.
lhs napply nat_add_zero_r.
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).
Proof.
rewrite nat_div_mod_spec''.
exact _.
Defined.
Proof.
rewrite nat_div_mod_spec''.
exact _.
Defined.
Definition nat_div_cancel_mul_l n m k
: 0 < k → (k × n) / (k × m) = n / m.
Proof.
intro kp.
destruct (nat_zero_or_gt_zero m) as [[] | mp].
1: by rewrite nat_mul_zero_r.
napply (nat_div_unique _ _ _ (k × (n mod m))).
1: rapply nat_mul_l_strictly_monotone.
rewrite <- nat_mul_assoc.
rewrite <- nat_dist_l.
apply ap.
symmetry; apply nat_div_mod_spec.
Defined.
: 0 < k → (k × n) / (k × m) = n / m.
Proof.
intro kp.
destruct (nat_zero_or_gt_zero m) as [[] | mp].
1: by rewrite nat_mul_zero_r.
napply (nat_div_unique _ _ _ (k × (n mod m))).
1: rapply nat_mul_l_strictly_monotone.
rewrite <- nat_mul_assoc.
rewrite <- nat_dist_l.
apply ap.
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.
Proof.
rewrite 2 (nat_mul_comm _ k).
napply nat_div_cancel_mul_l.
Defined.
: 0 < k → (n × k) / (m × k) = n / m.
Proof.
rewrite 2 (nat_mul_comm _ k).
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.
Proof.
intros H.
destruct (nat_zero_or_gt_zero m) as [[] | mp].
1: snapply nat_mul_zero_r.
rapply (nat_div_unique _ _ _ 0 _ _)^.
lhs napply nat_add_zero_r.
lhs napply nat_mul_assoc.
lhs napply (ap (fun x ⇒ x × _)).
1: napply nat_mul_comm.
lhs_V napply nat_mul_assoc.
snapply ap.
lhs_V napply nat_add_zero_r.
rhs napply (nat_div_mod_spec n m).
snapply ap.
symmetry.
rapply nat_mod_divides.
Defined.
Proof.
intros H.
destruct (nat_zero_or_gt_zero m) as [[] | mp].
1: snapply nat_mul_zero_r.
rapply (nat_div_unique _ _ _ 0 _ _)^.
lhs napply nat_add_zero_r.
lhs napply nat_mul_assoc.
lhs napply (ap (fun x ⇒ x × _)).
1: napply nat_mul_comm.
lhs_V napply nat_mul_assoc.
snapply ap.
lhs_V napply nat_add_zero_r.
rhs napply (nat_div_mod_spec n m).
snapply ap.
symmetry.
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.
Proof.
rewrite 2 (nat_mul_comm _ k).
snapply nat_div_mul_l.
Defined.
Definition nat_div_sub_mod n m : n / m = (n - n mod m) / m.
Proof.
destruct (nat_zero_or_gt_zero m) as [[] | mp].
1: reflexivity.
symmetry.
rewrite nat_div_mod_spec''.
rapply nat_div_mul_cancel_l.
Defined.
Proof.
rewrite 2 (nat_mul_comm _ k).
snapply nat_div_mul_l.
Defined.
Definition nat_div_sub_mod n m : n / m = (n - n mod m) / m.
Proof.
destruct (nat_zero_or_gt_zero m) as [[] | mp].
1: reflexivity.
symmetry.
rewrite nat_div_mod_spec''.
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).
Proof.
destruct (nat_zero_or_gt_zero k) as [[] | kp].
1: by rewrite nat_mul_zero_r.
destruct (nat_zero_or_gt_zero m) as [[] | mp].
1: snapply nat_div_zero_l.
apply nat_div_unique with (r := (n mod (m × k)) / m).
{ apply (lt_lt_leq_trans (m:=(m × k)/m)).
- rapply nat_div_strictly_monotone_r.
napply (nat_mod_lt_r' _ _ 0 _).
exact (nat_mul_strictly_monotone mp kp).
- by rewrite nat_div_mul_cancel_l. }
transitivity ((m × (k × (n / (m × k)))) / m + (n mod (m × k)) / m).
- f_ap.
symmetry; rapply nat_div_mul_cancel_l.
- rewrite nat_mul_assoc.
lhs_V napply nat_div_dist.
1: exact _.
apply (ap (fun x ⇒ x / m)).
symmetry; apply nat_div_mod_spec.
Defined.
Proof.
destruct (nat_zero_or_gt_zero k) as [[] | kp].
1: by rewrite nat_mul_zero_r.
destruct (nat_zero_or_gt_zero m) as [[] | mp].
1: snapply nat_div_zero_l.
apply nat_div_unique with (r := (n mod (m × k)) / m).
{ apply (lt_lt_leq_trans (m:=(m × k)/m)).
- rapply nat_div_strictly_monotone_r.
napply (nat_mod_lt_r' _ _ 0 _).
exact (nat_mul_strictly_monotone mp kp).
- by rewrite nat_div_mul_cancel_l. }
transitivity ((m × (k × (n / (m × k)))) / m + (n mod (m × k)) / m).
- f_ap.
symmetry; rapply nat_div_mul_cancel_l.
- rewrite nat_mul_assoc.
lhs_V napply nat_div_dist.
1: exact _.
apply (ap (fun x ⇒ x / m)).
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.
Proof.
intros [d r].
destruct (nat_zero_or_gt_zero k) as [[] | kp].
1: by rewrite nat_mul_zero_r, nat_div_zero_l.
destruct r.
rhs napply nat_div_cancel_mul_r.
2: exact _.
apply ap.
rapply nat_div_mul_cancel_r.
Defined.
Proof.
intros [d r].
destruct (nat_zero_or_gt_zero k) as [[] | kp].
1: by rewrite nat_mul_zero_r, nat_div_zero_l.
destruct r.
rhs napply nat_div_cancel_mul_r.
2: exact _.
apply ap.
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).
Proof.
rewrite (nat_div_sub_mod m k).
rapply nat_div_div_r.
Defined.
Proof.
rewrite (nat_div_sub_mod m 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).
Proof.
destruct (nat_zero_or_gt_zero k) as [[] | kp].
1: reflexivity.
destruct (nat_zero_or_gt_zero m) as [[] | mp].
1: by rewrite nat_mul_zero_r.
apply (nat_mod_unique _ _ (n / m)).
1: rapply nat_mul_l_strictly_monotone.
rewrite <- nat_mul_assoc.
rewrite <- nat_dist_l.
apply ap.
symmetry; apply nat_div_mod_spec.
Defined.
: (k × n) mod (k × m) = k × (n mod m).
Proof.
destruct (nat_zero_or_gt_zero k) as [[] | kp].
1: reflexivity.
destruct (nat_zero_or_gt_zero m) as [[] | mp].
1: by rewrite nat_mul_zero_r.
apply (nat_mod_unique _ _ (n / m)).
1: rapply nat_mul_l_strictly_monotone.
rewrite <- nat_mul_assoc.
rewrite <- nat_dist_l.
apply ap.
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.
Proof.
rewrite 3 (nat_mul_comm _ k).
napply nat_mod_mul_l.
Defined.
: (n × k) mod (m × k) = (n mod m) × k.
Proof.
rewrite 3 (nat_mul_comm _ k).
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.
Proof.
intros H p.
destruct p.
symmetry; rapply nat_div_mul_cancel_r.
Defined.
Definition nat_div_moveR_nV n m k : 0 < k → n = m × k → n / k = m.
Proof.
intros H p.
destruct p^.
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).
Proof.
intros H1 H2 [y q].
∃ y.
rewrite nat_div_mul_l; only 2: exact _.
by rapply nat_div_moveR_nV.
Defined.
Definition nat_divides_r_div n m l
: (n × l | m) → (n | m / l).
Proof.
destruct l; only 1: exact _.
intros [k p].
∃ k.
rapply nat_div_moveL_nV.
by lhs_V napply nat_mul_assoc.
Defined.
Definition nat_divides_l_mul n m l
: (l | m) → (n | m / l) → (n × l | m).
Proof.
intros H [k p].
∃ k.
rewrite nat_mul_assoc.
rewrite p.
rapply nat_mul_div_cancel_r.
Defined.
Proof.
intros H p.
destruct p.
symmetry; rapply nat_div_mul_cancel_r.
Defined.
Definition nat_div_moveR_nV n m k : 0 < k → n = m × k → n / k = m.
Proof.
intros H p.
destruct p^.
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).
Proof.
intros H1 H2 [y q].
∃ y.
rewrite nat_div_mul_l; only 2: exact _.
by rapply nat_div_moveR_nV.
Defined.
Definition nat_divides_r_div n m l
: (n × l | m) → (n | m / l).
Proof.
destruct l; only 1: exact _.
intros [k p].
∃ k.
rapply nat_div_moveL_nV.
by lhs_V napply nat_mul_assoc.
Defined.
Definition nat_divides_l_mul n m l
: (l | m) → (n | m / l) → (n × l | m).
Proof.
intros H [k p].
∃ k.
rewrite nat_mul_assoc.
rewrite p.
rapply nat_mul_div_cancel_r.
Defined.
The greatest common divisor of a number and 0 is the number itself.
Definition nat_gcd_zero_r n : nat_gcd n 0 = n.
Proof.
induction n; simpl; only 1: reflexivity.
by rewrite nat_sub_cancel.
Defined.
Proof.
induction n; simpl; only 1: reflexivity.
by rewrite nat_sub_cancel.
Defined.
The greatest common divisor of 1 and any number is 1.
The greatest common divisor of any number and 1 is 1.
Definition nat_gcd_one_r n : nat_gcd n 1 = 1.
Proof.
destruct n; trivial.
simpl.
destruct n; trivial.
rewrite nat_sub_succ_l; only 2: exact _.
by rewrite nat_sub_cancel.
Defined.
Proof.
destruct n; trivial.
simpl.
destruct n; trivial.
rewrite nat_sub_succ_l; only 2: exact _.
by rewrite nat_sub_cancel.
Defined.
Idempotency.
Definition nat_gcd_idem n : nat_gcd n n = n.
Proof.
induction n.
1: reflexivity.
unfold nat_gcd; fold nat_gcd.
by rewrite nat_mod_cancel.
Defined.
Proof.
induction n.
1: reflexivity.
unfold nat_gcd; fold nat_gcd.
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).
Proof.
revert n m; snapply nat_ind_strong; intros n IHn m.
destruct n.
1: split; exact _.
destruct (IHn (m mod n.+1) _ n.+1) as [H1 H2].
unfold nat_gcd; fold nat_gcd.
set (n' := n.+1) in ×.
split; only 1: exact H2.
set (r := m mod n'); rewrite (nat_div_mod_spec m n'); unfold r; clear r.
exact _.
Defined.
Proof.
revert n m; snapply nat_ind_strong; intros n IHn m.
destruct n.
1: split; exact _.
destruct (IHn (m mod n.+1) _ n.+1) as [H1 H2].
unfold nat_gcd; fold nat_gcd.
set (n' := n.+1) in ×.
split; only 1: exact H2.
set (r := m mod n'); rewrite (nat_div_mod_spec m n'); unfold r; clear r.
exact _.
Defined.
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).
Proof.
revert n m p; snapply nat_ind_strong; intros n IHn m p H1 H2.
destruct n; only 1: exact _.
unfold nat_gcd; fold nat_gcd.
apply IHn; only 1,3: exact _.
rewrite (nat_div_mod_spec m n.+1) in H2.
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).
Proof.
split; [intros [H1 H2] | intros H; split]; exact _.
Defined.
Proof.
revert n m p; snapply nat_ind_strong; intros n IHn m p H1 H2.
destruct n; only 1: exact _.
unfold nat_gcd; fold nat_gcd.
apply IHn; only 1,3: exact _.
rewrite (nat_div_mod_spec m n.+1) in H2.
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).
Proof.
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 : ∀ q, (q | n) → (q | m) → (q | p))
: (p | n) → (p | m) → nat_gcd n m = p.
Proof.
intros H1 H2.
rapply nat_divides_antisym.
Defined.
(H : ∀ q, (q | n) → (q | m) → (q | p))
: (p | n) → (p | m) → nat_gcd n m = p.
Proof.
intros H1 H2.
rapply nat_divides_antisym.
Defined.
As a corollary of uniqueness, we get that the greatest common divisor operation is commutative.
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.
Proof.
rapply nat_gcd_unique.
- rapply (nat_divides_trans (nat_divides_l_gcd_l _ _)).
- apply nat_divides_r_gcd; rapply nat_divides_trans.
Defined.
Proof.
rapply nat_gcd_unique.
- rapply (nat_divides_trans (nat_divides_l_gcd_l _ _)).
- apply nat_divides_r_gcd; rapply nat_divides_trans.
Defined.
Definition nat_gcd_is_zero_l n m : nat_gcd n m = 0 → n = 0.
Proof.
intros H.
generalize (nat_divides_l_gcd_l n m).
rewrite H.
intros [x p].
exact (p^ @ nat_mul_zero_r _).
Defined.
Proof.
intros H.
generalize (nat_divides_l_gcd_l n m).
rewrite H.
intros [x p].
exact (p^ @ nat_mul_zero_r _).
Defined.
Definition nat_gcd_is_zero_r n m : nat_gcd n m = 0 → m = 0.
Proof.
rewrite nat_gcd_comm.
apply nat_gcd_is_zero_l.
Defined.
Proof.
rewrite nat_gcd_comm.
apply nat_gcd_is_zero_l.
Defined.
Definition nat_gcd_zero_iff_zero n m : nat_gcd n m = 0 ↔ n = 0 ∧ m = 0.
Proof.
split.
- split.
+ by apply (nat_gcd_is_zero_l _ m).
+ by apply (nat_gcd_is_zero_r n).
- intros [-> ->].
reflexivity.
Defined.
Proof.
split.
- split.
+ by apply (nat_gcd_is_zero_l _ m).
+ by apply (nat_gcd_is_zero_r n).
- intros [-> ->].
reflexivity.
Defined.
nat_gcd is positive for positive inputs.
Instance nat_gcd_pos n m : 0 < n → 0 < m → 0 < nat_gcd n m.
Proof.
intros H1 H2.
apply lt_iff_not_geq.
intros H3; hnf in H3.
apply path_zero_leq_zero_r in H3.
apply nat_gcd_zero_iff_zero in H3.
destruct H3 as [->].
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.
Proof.
rapply nat_gcd_unique.
intros q H1 H2.
rapply nat_divides_r_gcd.
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.
Proof.
lhs napply nat_gcd_comm.
rhs napply nat_gcd_comm.
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.
Proof.
rhs_V exact (nat_gcd_l_add_r_mul n m 1).
by rewrite nat_mul_one_l.
Defined.
Definition nat_gcd_r_add_r n m : nat_gcd n (m + n) = nat_gcd n m.
Proof.
lhs napply nat_gcd_comm.
rhs napply nat_gcd_comm.
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.
Proof.
intros H.
lhs_V napply nat_gcd_l_add_r.
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.
Proof.
intros H.
lhs napply nat_gcd_comm.
rhs napply nat_gcd_comm.
rapply nat_gcd_l_sub.
Defined.
Proof.
intros H1 H2.
apply lt_iff_not_geq.
intros H3; hnf in H3.
apply path_zero_leq_zero_r in H3.
apply nat_gcd_zero_iff_zero in H3.
destruct H3 as [->].
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.
Proof.
rapply nat_gcd_unique.
intros q H1 H2.
rapply nat_divides_r_gcd.
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.
Proof.
lhs napply nat_gcd_comm.
rhs napply nat_gcd_comm.
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.
Proof.
rhs_V exact (nat_gcd_l_add_r_mul n m 1).
by rewrite nat_mul_one_l.
Defined.
Definition nat_gcd_r_add_r n m : nat_gcd n (m + n) = nat_gcd n m.
Proof.
lhs napply nat_gcd_comm.
rhs napply nat_gcd_comm.
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.
Proof.
intros H.
lhs_V napply nat_gcd_l_add_r.
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.
Proof.
intros H.
lhs napply nat_gcd_comm.
rhs napply nat_gcd_comm.
rapply nat_gcd_l_sub.
Defined.
Bezout's Identity
Definition NatBezout n m d : Type0
:= ∃ a b, a × n = d + b × m.
Existing Class NatBezout.
Instance nat_bezout_refl_l n k : NatBezout n k n.
Proof.
by ∃ 1, 0.
Defined.
:= ∃ a b, a × n = d + b × m.
Existing Class NatBezout.
Instance nat_bezout_refl_l n k : NatBezout n k n.
Proof.
by ∃ 1, 0.
Defined.
Definition nat_bezout_coprime n m : NatBezout n m 1 → nat_gcd n m = 1.
Proof.
intros [a [b p]].
rapply nat_gcd_unique.
intros q H1 H2.
rapply (nat_divides_add_l _ _ (b × m)).
destruct p; exact _.
Defined.
Definition nat_bezout_comm n m d
: 0 < m → NatBezout n m d → NatBezout m n d.
Proof.
intros H [a [b p]].
destruct (@equiv_leq_lt_or_eq 0 a _) as [|q].
- ∃ (n × a.+1 × b.+1 - b), (m × a.+1 × b.+1 - a).
rewrite 2 nat_dist_sub_r.
apply nat_moveR_nV.
rewrite <- nat_add_comm, nat_add_assoc, <- (nat_add_comm d).
rewrite <- nat_sub_l_add_r.
2: { apply nat_mul_r_monotone.
rewrite 2 nat_mul_succ_r.
napply (leq_trans _ (leq_add_l _ _)).
exact (leq_trans _ (leq_add_r _ _)). }
apply nat_moveL_nV.
rewrite nat_add_comm.
snapply (ap011 nat_add p).
lhs napply nat_mul_comm.
rhs_V napply nat_mul_assoc.
rhs_V napply nat_mul_assoc.
snapply ap.
lhs_V napply nat_mul_assoc.
rhs napply nat_mul_assoc.
apply nat_mul_comm.
- destruct q.
∃ 0, 0.
rewrite 2 nat_mul_zero_l, nat_add_zero_r in ×.
symmetry in p; symmetry.
apply equiv_nat_add_zero in p.
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).
Proof.
pose (k := n + m); assert (p : n + m = k) by reflexivity; clearbody k.
revert k n m p; snapply nat_ind_strong; hnf; intros k IHk n m q H.
Proof.
intros [a [b p]].
rapply nat_gcd_unique.
intros q H1 H2.
rapply (nat_divides_add_l _ _ (b × m)).
destruct p; exact _.
Defined.
Definition nat_bezout_comm n m d
: 0 < m → NatBezout n m d → NatBezout m n d.
Proof.
intros H [a [b p]].
destruct (@equiv_leq_lt_or_eq 0 a _) as [|q].
- ∃ (n × a.+1 × b.+1 - b), (m × a.+1 × b.+1 - a).
rewrite 2 nat_dist_sub_r.
apply nat_moveR_nV.
rewrite <- nat_add_comm, nat_add_assoc, <- (nat_add_comm d).
rewrite <- nat_sub_l_add_r.
2: { apply nat_mul_r_monotone.
rewrite 2 nat_mul_succ_r.
napply (leq_trans _ (leq_add_l _ _)).
exact (leq_trans _ (leq_add_r _ _)). }
apply nat_moveL_nV.
rewrite nat_add_comm.
snapply (ap011 nat_add p).
lhs napply nat_mul_comm.
rhs_V napply nat_mul_assoc.
rhs_V napply nat_mul_assoc.
snapply ap.
lhs_V napply nat_mul_assoc.
rhs napply nat_mul_assoc.
apply nat_mul_comm.
- destruct q.
∃ 0, 0.
rewrite 2 nat_mul_zero_l, nat_add_zero_r in ×.
symmetry in p; symmetry.
apply equiv_nat_add_zero in p.
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).
Proof.
pose (k := n + m); assert (p : n + m = k) by reflexivity; clearbody k.
revert k n m p; snapply nat_ind_strong; hnf; intros k IHk n m q H.
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' : ∀ n' m', n + m = n' + m' → 0 < n' → n' < m'
→ NatBezout n' m' (nat_gcd n' m')).
{ intros n' m' p H1 H2; destruct q.
assert (m' < n + m) by (rewrite p; change (0 + m' < n' + m'); exact _).
destruct (IHk m' _ n' (m' - n') (nat_add_sub_r_cancel _) _) as [a [b r]].
∃ (a + b), b.
rewrite nat_dist_r, r, nat_dist_sub_l, <- nat_add_assoc.
rewrite nat_add_sub_l_cancel; only 2: rapply nat_mul_l_monotone.
snapply (ap (fun x ⇒ x + _)).
rapply nat_gcd_r_sub. }
destruct (nat_trichotomy n m) as [[l | p] | r].
- by apply H'.
- destruct p.
rewrite nat_gcd_idem; exact _.
- destruct (@equiv_leq_lt_or_eq 0 m _).
+ rewrite nat_gcd_comm.
rapply nat_bezout_comm.
rapply H'.
apply nat_add_comm.
+ destruct p.
rewrite nat_gcd_zero_r; exact _.
Defined.
→ NatBezout n' m' (nat_gcd n' m')).
{ intros n' m' p H1 H2; destruct q.
assert (m' < n + m) by (rewrite p; change (0 + m' < n' + m'); exact _).
destruct (IHk m' _ n' (m' - n') (nat_add_sub_r_cancel _) _) as [a [b r]].
∃ (a + b), b.
rewrite nat_dist_r, r, nat_dist_sub_l, <- nat_add_assoc.
rewrite nat_add_sub_l_cancel; only 2: rapply nat_mul_l_monotone.
snapply (ap (fun x ⇒ x + _)).
rapply nat_gcd_r_sub. }
destruct (nat_trichotomy n m) as [[l | p] | r].
- by apply H'.
- destruct p.
rewrite nat_gcd_idem; exact _.
- destruct (@equiv_leq_lt_or_eq 0 m _).
+ rewrite nat_gcd_comm.
rapply nat_bezout_comm.
rapply H'.
apply nat_add_comm.
+ destruct p.
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).
Proof.
intros H1 H2; split; [| apply nat_bezout_comm]; exact _.
Defined.
: 0 < n → 0 < m
→ NatBezout n m (nat_gcd n m) ∧ NatBezout m n (nat_gcd n m).
Proof.
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).
Proof.
destruct n; [ right | left ]; exact _.
Defined.
: NatBezout n m (nat_gcd n m) + NatBezout m n (nat_gcd n m).
Proof.
destruct n; [ right | left ]; exact _.
Defined.
Least common multiple
The least common multiple of 0 and n is 0.
The least common multiple of n and 0 is 0.
Definition nat_lcm_zero_r n : nat_lcm n 0 = 0.
Proof.
unfold nat_lcm.
by rewrite nat_div_zero_l, nat_mul_zero_r.
Defined.
Proof.
unfold nat_lcm.
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.
Proof.
unfold nat_lcm.
by rewrite nat_gcd_one_l, nat_div_one_r, nat_mul_one_l.
Defined.
Proof.
unfold nat_lcm.
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.
Proof.
unfold nat_lcm.
by rewrite nat_gcd_one_r, nat_div_one_r, nat_mul_one_r.
Defined.
Proof.
unfold nat_lcm.
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.
Proof.
unfold nat_lcm.
by rewrite nat_gcd_idem, nat_mul_div_cancel_l.
Defined.
Proof.
unfold nat_lcm.
by rewrite nat_gcd_idem, nat_mul_div_cancel_l.
Defined.
Instance nat_divides_r_lcm_r n m : (m | nat_lcm n m).
Proof.
unfold nat_lcm.
rewrite nat_div_mul_l; only 2: exact _.
rewrite <- nat_div_mul_r; exact _.
Defined.
Proof.
unfold nat_lcm.
rewrite nat_div_mul_l; only 2: exact _.
rewrite <- nat_div_mul_r; exact _.
Defined.
Instance nat_divides_l_lcm n m k : (n | k) → (m | k) → (nat_lcm n m | k).
Proof.
intros H1 H2.
destruct (equiv_leq_lt_or_eq (n:=0) (m:=n) _) as [lt_n | p];
only 2: by destruct p.
destruct (equiv_leq_lt_or_eq (n:=0) (m:=m) _) as [lt_m | q];
only 2: (destruct q; by rewrite nat_lcm_zero_r).
unfold nat_lcm.
destruct (nat_bezout_pos_l n m _) as [a [b p]].
apply nat_moveR_nV in p.
rewrite nat_div_mul_l.
2: exact _.
rapply nat_divides_l_div.
destruct p.
rewrite nat_dist_sub_l.
napply nat_divides_sub.
1: rewrite nat_mul_comm.
1,2: exact _.
Defined.
Definition nat_divides_l_iff_divides_l_lcm n m k
: (n | k) × (m | k) ↔ (nat_lcm n m | k).
Proof.
split.
- intros [H1 H2]; exact _.
- intros H; split.
+ rapply (nat_divides_trans _ H).
+ exact _.
Defined.
Proof.
intros H1 H2.
destruct (equiv_leq_lt_or_eq (n:=0) (m:=n) _) as [lt_n | p];
only 2: by destruct p.
destruct (equiv_leq_lt_or_eq (n:=0) (m:=m) _) as [lt_m | q];
only 2: (destruct q; by rewrite nat_lcm_zero_r).
unfold nat_lcm.
destruct (nat_bezout_pos_l n m _) as [a [b p]].
apply nat_moveR_nV in p.
rewrite nat_div_mul_l.
2: exact _.
rapply nat_divides_l_div.
destruct p.
rewrite nat_dist_sub_l.
napply nat_divides_sub.
1: rewrite nat_mul_comm.
1,2: exact _.
Defined.
Definition nat_divides_l_iff_divides_l_lcm n m k
: (n | k) × (m | k) ↔ (nat_lcm n m | k).
Proof.
split.
- intros [H1 H2]; exact _.
- intros H; split.
+ rapply (nat_divides_trans _ H).
+ 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 : ∀ q, (n | q) → (m | q) → (k | q))
: (n | k) → (m | k) → nat_lcm n m = k.
Proof.
intros H1 H2.
rapply nat_divides_antisym.
Defined.
(H : ∀ q, (n | q) → (m | q) → (k | q))
: (n | k) → (m | k) → nat_lcm n m = k.
Proof.
intros H1 H2.
rapply nat_divides_antisym.
Defined.
As a corollary of uniqueness, we get that the least common multiple operation is commutative.
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.
Proof.
rapply nat_lcm_unique.
intros q H1 H2.
rapply nat_divides_l_lcm.
rapply nat_divides_l_lcm.
rapply (nat_divides_trans _ H2).
Defined.
Proof.
rapply nat_lcm_unique.
intros q H1 H2.
rapply nat_divides_l_lcm.
rapply nat_divides_l_lcm.
rapply (nat_divides_trans _ H2).
Defined.
Class IsPrime (n : nat) : Type0 := {
gt_one_isprime :: 1 < n;
isprime : ∀ m, (m | n) → (m = 1) + (m = n);
}.
Definition issig_IsPrime n : _ <~> IsPrime n := ltac:(issig).
Instance ishprop_isprime `{Funext} n : IsHProp (IsPrime n).
Proof.
napply istrunc_equiv_istrunc.
1: apply issig_IsPrime.
rapply istrunc_sigma.
intros H1.
snapply istrunc_forall.
intros m.
snapply istrunc_forall.
intros d.
rapply ishprop_sum.
intros p q.
napply (snd neq_iff_lt_or_gt _ (p^ @ q)).
by left.
Defined.
gt_one_isprime :: 1 < n;
isprime : ∀ m, (m | n) → (m = 1) + (m = n);
}.
Definition issig_IsPrime n : _ <~> IsPrime n := ltac:(issig).
Instance ishprop_isprime `{Funext} n : IsHProp (IsPrime n).
Proof.
napply istrunc_equiv_istrunc.
1: apply issig_IsPrime.
rapply istrunc_sigma.
intros H1.
snapply istrunc_forall.
intros m.
snapply istrunc_forall.
intros d.
rapply ishprop_sum.
intros p q.
napply (snd neq_iff_lt_or_gt _ (p^ @ q)).
by left.
Defined.
0 is not a prime number.
1 is not a prime number.
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.
First we begin by discarding the n = 0 case as we can easily prove that 0 is not prime.
Next, we rewrite IsPrime n.+1 as the equivalent sigma type.
The condition in the first component in IsPrime is clearly decidable, so we can proceed to the second component.
napply decidable_equiv'.
1: exact (equiv_sigma_prod0 _ _)^-1%equiv.
snapply decidable_prod.
1: exact _.
1: exact (equiv_sigma_prod0 _ _)^-1%equiv.
snapply decidable_prod.
1: exact _.
In order to show that this ∀ 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).
pose (l := list_filter (seq n.+2) (fun x ⇒ (x | n.+1)) _).
rapply (decidable_iff (A := for_all P l)).
split.
- intros Pl x d.
apply inlist_for_all with l x in Pl.
1: exact Pl.
apply inlist_filter.
split; only 2: assumption.
apply inlist_seq.
apply leq_divides in d.
1,2: exact _.
- intros H.
apply for_all_inlist.
intros x H'.
apply inlist_filter in H'.
destruct H' as [p H'].
apply inlist_seq in p.
rapply H.
Defined.
pose (l := list_filter (seq n.+2) (fun x ⇒ (x | n.+1)) _).
rapply (decidable_iff (A := for_all P l)).
split.
- intros Pl x d.
apply inlist_for_all with l x in Pl.
1: exact Pl.
apply inlist_filter.
split; only 2: assumption.
apply inlist_seq.
apply leq_divides in d.
1,2: exact _.
- intros H.
apply for_all_inlist.
intros x H'.
apply inlist_filter in H'.
destruct H' as [p H'].
apply inlist_seq in p.
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).
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).
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.
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.
Definition nat_coprime_iff_not_divides (p : Prime) n
: nat_gcd p n = 1 ↔ ¬ (p | n).
Proof.
split.
- intros q [d r].
destruct r.
rewrite (nat_gcd_r_add_r_mul p 0) in q.
rewrite nat_gcd_zero_r in q.
apply (@neq_iff_lt_or_gt p 1).
1: right; exact _.
exact q.
- intros nd.
rapply nat_gcd_unique.
intros q H1 H2.
apply isprime in H1.
destruct H1 as [H1|H1].
+ destruct H1; exact _.
+ destruct H1; contradiction.
Defined.
: nat_gcd p n = 1 ↔ ¬ (p | n).
Proof.
split.
- intros q [d r].
destruct r.
rewrite (nat_gcd_r_add_r_mul p 0) in q.
rewrite nat_gcd_zero_r in q.
apply (@neq_iff_lt_or_gt p 1).
1: right; exact _.
exact q.
- intros nd.
rapply nat_gcd_unique.
intros q H1 H2.
apply isprime in H1.
destruct H1 as [H1|H1].
+ destruct H1; exact _.
+ 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).
Proof.
intros d.
destruct (dec (p | n)) as [H|H].
1: by left.
right.
apply nat_coprime_iff_not_divides in H.
destruct (nat_bezout_pos_l p n _) as [x [y q]].
destruct H^; clear H.
destruct d as [d r].
∃ (x × m - y × d).
lhs napply nat_dist_sub_r.
rewrite <- 2 nat_mul_assoc.
rewrite <- (nat_mul_comm p).
destruct r^; clear r.
rewrite 2 nat_mul_assoc.
lhs_V napply nat_dist_sub_r.
rhs_V napply nat_mul_one_l.
apply (ap (fun x ⇒ nat_mul x m)).
apply nat_moveR_nV.
exact q.
Defined.
: (p | n × m) → (p | n) + (p | m).
Proof.
intros d.
destruct (dec (p | n)) as [H|H].
1: by left.
right.
apply nat_coprime_iff_not_divides in H.
destruct (nat_bezout_pos_l p n _) as [x [y q]].
destruct H^; clear H.
destruct d as [d r].
∃ (x × m - y × d).
lhs napply nat_dist_sub_r.
rewrite <- 2 nat_mul_assoc.
rewrite <- (nat_mul_comm p).
destruct r^; clear r.
rewrite 2 nat_mul_assoc.
lhs_V napply nat_dist_sub_r.
rhs_V napply nat_mul_one_l.
apply (ap (fun x ⇒ nat_mul x m)).
apply nat_moveR_nV.
exact q.
Defined.
Composite Numbers
Class IsComposite n : Type0
:= iscomposite : ∃ a, 1 < a < n ∧ (a | n).
Definition gt_1_iscomposite@{} n : IsComposite n → 1 < n.
Proof.
intros [a [[H1 H2] H3]].
exact _.
Defined.
Hint Immediate gt_1_iscomposite : typeclass_instances.
:= iscomposite : ∃ a, 1 < a < n ∧ (a | n).
Definition gt_1_iscomposite@{} n : IsComposite n → 1 < n.
Proof.
intros [a [[H1 H2] H3]].
exact _.
Defined.
Hint Immediate gt_1_iscomposite : typeclass_instances.
Being composite is a decidable property.
Instance decidable_iscomposite@{} n : Decidable (IsComposite n).
Proof.
unfold IsComposite.
rapply (decidable_exists_nat n).
intros k c.
exact (snd (fst c)).
Defined.
Proof.
unfold IsComposite.
rapply (decidable_exists_nat n).
intros k c.
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.
Proof.
split.
- intros H.
split; only 1: exact _.
intros [a [[H2 H3] H4]].
apply isprime in H4.
destruct H4 as [H4|H4]; destruct H4; exact (lt_irrefl _ _).
- intros [H1 H].
rapply Build_IsPrime.
intros m d.
destruct (dec (1 < d.1)) as [H2|H2].
+ pose proof (divides_divisor _ _ d) as d'.
apply leq_divides in d'.
2: exact _.
apply equiv_leq_lt_or_eq in d'.
destruct d' as [d'|d'].
× assert (H' : IsComposite n).
{ ∃ d.1.
split; only 1: split; exact _. }
contradiction H.
× destruct d as [d r].
simpl in ×.
destruct d'.
left.
rewrite <- nat_div_cancel with d.
2: exact _.
rewrite <- nat_div_mul_cancel_l with d m.
2: exact _.
by apply (ap (fun x ⇒ x / d)).
+ apply geq_iff_not_lt in H2.
destruct d as [d r].
simpl in *; hnf in H2.
destruct d.
{ rewrite nat_mul_zero_l in r.
destruct n.
1: contradiction (not_lt_zero_r _ H1).
contradiction (neq_nat_zero_succ _ r). }
destruct d.
{ rewrite nat_mul_one_l in r.
by right. }
apply leq_pred' in H2.
contradiction (not_lt_zero_r d).
Defined.
: IsPrime n ↔ 1 < n ∧ ¬ IsComposite n.
Proof.
split.
- intros H.
split; only 1: exact _.
intros [a [[H2 H3] H4]].
apply isprime in H4.
destruct H4 as [H4|H4]; destruct H4; exact (lt_irrefl _ _).
- intros [H1 H].
rapply Build_IsPrime.
intros m d.
destruct (dec (1 < d.1)) as [H2|H2].
+ pose proof (divides_divisor _ _ d) as d'.
apply leq_divides in d'.
2: exact _.
apply equiv_leq_lt_or_eq in d'.
destruct d' as [d'|d'].
× assert (H' : IsComposite n).
{ ∃ d.1.
split; only 1: split; exact _. }
contradiction H.
× destruct d as [d r].
simpl in ×.
destruct d'.
left.
rewrite <- nat_div_cancel with d.
2: exact _.
rewrite <- nat_div_mul_cancel_l with d m.
2: exact _.
by apply (ap (fun x ⇒ x / d)).
+ apply geq_iff_not_lt in H2.
destruct d as [d r].
simpl in *; hnf in H2.
destruct d.
{ rewrite nat_mul_zero_l in r.
destruct n.
1: contradiction (not_lt_zero_r _ H1).
contradiction (neq_nat_zero_succ _ r). }
destruct d.
{ rewrite nat_mul_one_l in r.
by right. }
apply leq_pred' in H2.
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.
Proof.
napply iff_compose.
- napply iff_functor_prod.
1: exact iff_refl.
napply iff_compose.
+ apply iff_not.
rapply isprime_iff_not_iscomposite.
+ rapply iff_not_prod.
- napply iff_compose.
1: napply sum_distrib_l.
napply iff_compose.
+ napply iff_functor_sum.
1: apply iff_contradiction.
napply iff_functor_prod.
1: exact iff_refl.
rapply iff_stable.
+ napply iff_compose.
1: rapply sum_empty_l.
split; only 1: exact snd.
intros H; split; only 2: exact H.
exact _.
Defined.
: 1 < n ∧ ¬ IsPrime n ↔ IsComposite n.
Proof.
napply iff_compose.
- napply iff_functor_prod.
1: exact iff_refl.
napply iff_compose.
+ apply iff_not.
rapply isprime_iff_not_iscomposite.
+ rapply iff_not_prod.
- napply iff_compose.
1: napply sum_distrib_l.
napply iff_compose.
+ napply iff_functor_sum.
1: apply iff_contradiction.
napply iff_functor_prod.
1: exact iff_refl.
rapply iff_stable.
+ napply iff_compose.
1: rapply sum_empty_l.
split; only 1: exact snd.
intros H; split; only 2: exact H.
exact _.
Defined.
Definition exists_prime_divisor@{} n
: 1 < n → ∃ (p : Prime), (p | n).
Proof.
revert n; snapply nat_ind_strong; hnf; intros n IHn H.
destruct (dec (IsPrime n)) as [x|x].
1: ∃ (_; x); exact _.
pose (r := (H, x)).
apply not_isprime_iff_iscomposite in r.
destruct r as [d [[H1 H2] H3]].
destruct (IHn d _ _) as [p r].
∃ p.
exact _.
Defined.
: 1 < n → ∃ (p : Prime), (p | n).
Proof.
revert n; snapply nat_ind_strong; hnf; intros n IHn H.
destruct (dec (IsPrime n)) as [x|x].
1: ∃ (_; x); exact _.
pose (r := (H, x)).
apply not_isprime_iff_iscomposite in r.
destruct r as [d [[H1 H2] H3]].
destruct (IHn d _ _) as [p r].
∃ p.
exact _.
Defined.
Any natural number can either be written as a product of primes or is zero.
Definition prime_factorization@{} n
: 0 < n
→ ∃ (l : list Prime),
n = fold_right (fun (p : Prime) n ⇒ nat_mul p n) 1 l.
Proof.
revert n; snapply nat_ind_strong; hnf; intros n IHn H.
destruct H as [|n IH].
1: ∃ nil; reflexivity.
destruct (exists_prime_divisor n.+1 _) as [p d].
pose proof (l := lt_divides d.1 n.+1 _ _ _).
destruct d as [k H].
destruct (IHn k l) as [f r].
{ destruct H, k.
1: contradiction (lt_irrefl 0).
exact _. }
∃ (p :: f)%list.
simpl; destruct r.
symmetry.
lhs napply nat_mul_comm.
exact H.
Defined.
: 0 < n
→ ∃ (l : list Prime),
n = fold_right (fun (p : Prime) n ⇒ nat_mul p n) 1 l.
Proof.
revert n; snapply nat_ind_strong; hnf; intros n IHn H.
destruct H as [|n IH].
1: ∃ nil; reflexivity.
destruct (exists_prime_divisor n.+1 _) as [p d].
pose proof (l := lt_divides d.1 n.+1 _ _ _).
destruct d as [k H].
destruct (IHn k l) as [f r].
{ destruct H, k.
1: contradiction (lt_irrefl 0).
exact _. }
∃ (p :: f)%list.
simpl; destruct r.
symmetry.
lhs napply nat_mul_comm.
exact H.
Defined.
TODO: show that any two prime factorizations are unique up to permutation of the lists.