# Library Coqtail.Arith.Ndiv

Require Import Arith.
Require Import Euclid.
Require Export Nle.
Require Export Nk_ind.
Require Export Compare.
Open Scope nat_scope.

# Definitions

Definition of divisibility
Inductive Ndivide a b : Prop :=
| Ndivide_intro : q, b = q × aNdivide a b.

Definition of a quotient
Inductive Nquotient a b : natProp :=
| Nquotient_intro : q, b = q × aNquotient a b q.

Definition of modulus/remainder
Inductive Nmod a b : natProp :=
| Nmod_intro : q r, b = q × a + rr < aNmod a b r.

Notation
Notation "( a | b )" := (Ndivide a b) (at level 0) : nat_scope.

Definition of coprimality
Definition Nrel_prime p q := n, (n | p)(n | q)n = 1.

Definition of primality
Definition Nprime p := 1<p ( n, 1 < n < p¬ (n | p)).

# Basic results on prime numbers

0 is not prime
Lemma Nnot_prime_0 : ~(Nprime 0).
Proof.
unfold Nprime.
intro.
destruct H.
apply le_Sn_O in H.
exact H.
Qed.

1 is not prime
Lemma Nnot_prime_1 : ~(Nprime 1).
Proof.
unfold Nprime.
intro.
destruct H.
apply lt_irrefl in H.
exact H.
Qed.

A prime number is greater than or equal to 2
Lemma Nprime_ge_2 : (p:nat), Nprime p → 2p.
Proof.
intros.
destruct p.
apply Nnot_prime_0 in H.
destruct p.
apply Nnot_prime_1 in H.
unfold Nprime in H.
destruct H.
auto with arith.
Qed.

A composed number is not prime
Lemma Ncomposed_not_prime : n m, 1 < n → 1 < m~(Nprime (n × m)).
Proof.
intros.
intro.
destruct H1.
apply H2 with n.
split.
auto with arith.
replace n with (n×1).
destruct n.
apply le_Sn_O in H.
rewrite <- mult_assoc.
apply mult_S_lt_compat_l.
rewrite mult_1_l.
trivial.
auto with arith.
m.
ring.
Qed.

# Basic properties of divisibility

Lemma Ndiv_plus_compat : p a b, (p | a)(p | b)(p | a + b).
Proof.
intros.
destruct H.
destruct H0.
apply Ndivide_intro with (q+q0).
rewrite H. rewrite H0.
ring.
Qed.

Product divisiblity weakening
Lemma Nab_div_c : a b c, (a × b | c)(a | c).
Proof.
intros.
destruct H.
apply Ndivide_intro with (q×b).
rewrite H.
ring.
Qed.

A divisor is usually nonzero
Lemma Ndiv_non_0 : a b, (a | b) → 1 b → 1 a.
Proof.
intros.
destruct a.
destruct H.
rewrite mult_0_r in H.
rewrite H in H0.
exact H0.
auto with arith.
Qed.

Any number divides 0
Lemma Ndiv_0 : a, (a | 0).
intros.
apply Ndivide_intro with 0.
ring.
Qed.

1 divides any number
Lemma Ndiv_1 : a, (1 | a).
intros.
apply Ndivide_intro with a.
ring.
Qed.

Not divisor implies nonzero
Lemma Nnon_div_non_zero : a b, ¬( a | b)b > 0.
intros.
destruct b.
destruct H.
apply Ndiv_0.
auto with arith.
Qed.

n divides n
Lemma Ndiv_n_n : n, (n|n).
Proof.
intro.
apply Ndivide_intro with 1.
ring.
Qed.

# Basic properties of quotient

Quotient implies divisibility
Lemma Nquotient_div : a b q, Nquotient a b q(a | b).
Proof.
intros.
destruct H.
apply Ndivide_intro with q.
auto.
Qed.

Compatibility with order
Lemma Nquotient_le_compat : a b c q p,
Nquotient a b qNquotient a c p → 1 b cq p.
Proof.
intros.
assert (1a).
apply Ndiv_non_0 with b.
apply Nquotient_div with q.
exact H.
destruct H1.
exact H1.
assert ( a',a=S a').
destruct a.
apply le_Sn_O in H2.
a.
reflexivity.
destruct H3.
destruct H.
destruct H0.
destruct H1.
rewrite H in H4.
rewrite H0 in H4.
rewrite H3 in H4.
apply mult_S_le_reg_l with x.
assert (S x×q=q×S x).
ring.
assert (S x×q0=q0×S x).
ring.
rewrite H5.
rewrite H6.
exact H4.
Qed.

# Properties of divisibility

Transitivity
Lemma Ndiv_trans : a b c, (a | b)(b | c)(a | c).
Proof.
intros.
destruct H.
destruct H0.
(q×q0).
rewrite H0.
rewrite H.
ring.
Qed.

Lemma Ndiv_plus_simpl : a b c, (a | b + c)(a | b)(a | c).
Proof.
intros.
destruct b.
destruct H.
apply Ndivide_intro with q.
auto with arith.

destruct H.
destruct H0.
apply Ndivide_intro with (q-q0).
assert (q0q).
apply Nquotient_le_compat with a (S b) (S b+c).
apply Nquotient_intro. exact H0.
apply Nquotient_intro. exact H.
split.
auto with arith.
auto with arith.
apply Nle_plus in H1.
destruct H1.
rewrite H1.
assert (q0+x-q0=x).
apply minus_plus.
rewrite H2.
rewrite H1 in H.
rewrite H0 in H.
rewrite mult_plus_distr_r in H.
rewrite plus_comm in H.
apply plus_reg_l with (q0×a).
rewrite plus_comm.
rewrite H.
auto with arith.
Qed.

Right implification of subtraction
Lemma Ndiv_minus_simpl_r : a b c, b c(a | b - c)(a | c)(a | b).
Proof.
intros.
apply Nle_plus in H.
destruct H.
rewrite H in × |- ×.
rewrite minus_plus in H0.
apply Ndiv_plus_compat; auto.
Qed.

Left implification of subtraction
Lemma Ndiv_minus_simpl_l : a b c, b c(a | b - c)(a | b)(a | c).
Proof.
intros.
apply Nle_plus in H.
destruct H.
rewrite H in × |- ×.
rewrite minus_plus in H0.
rewrite plus_comm in H1.
apply Ndiv_plus_simpl with x; auto.
Qed.

Weak compatibility with multiplication
Lemma Ndiv_mult_compat : a b q, (a | b)(a | b × q).
Proof.
intros.
destruct H.
apply Ndivide_intro with (q0×q).
rewrite H.
ring.
Qed.

Strong compatibility with multiplication
Lemma Ndiv_strong_mult_compat : a b q, (a|b)(a × q | b × q).
Proof.
intros.
destruct H.
apply Ndivide_intro with (q0).
rewrite H.
ring.
Qed.

Simplification of common factor
Lemma Ndiv_mult_simpl : a b q, q 0 → (a × q | b × q)(a | b).
Proof.
intros.
destruct H0.
destruct q.
reflexivity.
rewrite mult_assoc in H0.
assert (S q×b=S q*(q0×a)).
rewrite mult_comm.
rewrite H0.
ring.
assert (b=q0×a).
apply toto with q.
rewrite mult_comm.
rewrite H0.
ring.
apply Ndivide_intro with q0.
auto.
Qed.

Divisibility implies order
Lemma Ndiv_le : n p, 0 < p(n | p)n p.
Proof.
intros.
destruct H0.
destruct p.
apply lt_irrefl in H. contradiction.
destruct n.
auto with arith.
destruct q.
simpl in H0.
discriminate H0.
replace (S n) with (1×S n).
rewrite H0.
apply mult_le_compat.
auto with arith.
auto with arith.
rewrite mult_1_l.
trivial.
Qed.

Dividable by 0 implies zero
Lemma Ndiv_0_n : n, (0 | n)n = 0.
Proof.
destruct n.
trivial.
intro.
destruct H.
rewrite mult_0_r in H.
discriminate H.
Qed.

# Properties of coprimes

n and n are usually not coprime
Lemma Nnon_rel_prime_n_n : n, n 1 → ~(Nrel_prime n n).
Proof.
intro.
intro.
intro.
unfold Nrel_prime in H0.
assert (n=1).
apply H0.
apply Ndiv_n_n.
apply Ndiv_n_n.
Qed.

Compatibility with modulus
Theorem Nrel_prime_mod : a b r, Nrel_prime a bNmod a b rNrel_prime a r.
Proof.
intros.
destruct H0.
unfold Nrel_prime in H.
unfold Nrel_prime.
intros.
assert (n|b).
rewrite H0.
apply Ndiv_plus_compat.
rewrite mult_comm.
apply Ndiv_mult_compat.
auto.
auto.
apply H.
auto.
auto.
Qed.

Commutativity
Lemma Nrel_prime_comm : a b, Nrel_prime a bNrel_prime b a.
Proof.
intros.
intro.
intros.
apply H.
auto.
auto.
Qed.

Weakening from primality to coprimality
Lemma Nprime_le_rel_prime : n p, Nprime p → 1 < n < pNrel_prime n p.
Proof.
intros.
destruct H0.
destruct H.
intro.
intros.
assert (0<n0).
apply Ndiv_non_0 with n.
auto.
auto with arith.
assert (n0<p).
apply le_trans with (S n).
apply le_n_S.
apply Ndiv_le.
auto with arith.
trivial.
auto.
destruct n0.
apply Ndiv_0_n in H3.
rewrite H3 in H0.
inversion H0.
destruct n0.
trivial.
apply H2 in H4.
split.
auto with arith.
auto.
Qed.

A coprime of 0 is 1
Lemma Nrel_prime_0 : n, Nrel_prime n 0 → n = 1.
Proof.
intros.
apply H.
apply Ndiv_n_n.
apply Ndiv_0.
Qed.

Any number is coprime with 1
Lemma Nrel_prime_1 : n, Nrel_prime n 1.
Proof.
intros.
intro.
intros.
destruct n0.
destruct H0.
rewrite mult_0_r in H0. auto.
apply Ndiv_le in H0.
destruct n0.
auto.
inversion H0.
inversion H2.
auto.
Qed.

# Gauss theorem

Theorem Ngauss : a b c, (a | b × c)Nrel_prime a b(a | c).
Proof.
apply (nat_strong_ind (fun a b c, (a|b×c)Nrel_prime a b(a|c))).
intros.
destruct H.
rewrite mult_0_r in H.
apply mult_is_O in H.
destruct H.
rewrite H in H0.
apply Nnon_rel_prime_n_n in H0.
auto with arith.
rewrite H.
apply Ndiv_0.

intros.
destruct n.
apply Ndiv_1.

destruct H0.
assert (diveucl b (S (S n))).
apply eucl_dev.
auto with arith.
destruct H2.
assert (diveucl c (S(S n))).
apply eucl_dev.
auto with arith.
destruct H2.
rewrite e in H0.
rewrite e0 in H0.
rewrite mult_plus_distr_l in H0.
rewrite mult_plus_distr_r in H0.
rewrite mult_plus_distr_r in H0.
assert (S (S n)|r×r0).
apply Ndiv_plus_simpl with (q0 ×S( S n) × r0).
apply Ndiv_plus_simpl with (r × (q1 × S(S n))).
apply Ndiv_plus_simpl with (q0 × S(S n) × (q1 × S(S n))).
apply Ndivide_intro with q.
rewrite <- H0.
ring.
apply Ndivide_intro with (q0×S(S n)×q1).
ring.
apply Ndivide_intro with (r×q1).
ring.
apply Ndivide_intro with (r0×q0).
ring.
destruct H2.
assert (Nrel_prime (S(S n)) r).
apply Nrel_prime_mod with b.
auto.
apply Nmod_intro with q0.
auto.
auto.
assert (r|q2).
apply H with (S(S n)).
auto with arith.
apply Ndivide_intro with r0.
rewrite mult_comm.
rewrite <- H2.
ring.
apply Nrel_prime_comm.
auto.
assert (S(S n)×r | r×r0).
rewrite H2.
rewrite mult_comm.
apply Ndiv_strong_mult_compat.
auto.
assert (S(S n)|r0).
apply Ndiv_mult_simpl with r.
destruct r.
rewrite plus_0_r in e.
assert (S(S n)|b).
apply Ndivide_intro with q0.
auto.
assert (S(S n)=1).
apply H1.
apply Ndiv_n_n.
auto.
discriminate H7.
auto with arith.
destruct H5.
apply Ndivide_intro with q3.
rewrite mult_comm.
rewrite H5.
ring.
rewrite e0.
apply Ndiv_plus_compat.
rewrite mult_comm.
apply Ndiv_mult_compat.
apply Ndiv_n_n.
auto.
Qed.

# Decidability of divisibility

Algorithm to compute a remainder modulus a number
Fixpoint Ndiv_mod_algo (n m:nat) {struct m} : nat :=
match n with
| 0 ⇒ 0
| S n'
match m with
| 0 ⇒ 0
| S m'
let tmp:=S (Ndiv_mod_algo n m') in
match beq_nat n tmp with
| true ⇒ 0
| falsetmp
end
end
end.

Algorithm to decide divisibility
Definition Ndiv_algo (n m:nat) : bool :=
beq_nat (Ndiv_mod_algo n m) 0.

m mod n equals m if n is greater than m
Lemma Ndiv_mod_l0 : n m, m < nNdiv_mod_algo n m = m.
Proof.
induction m.
intros. destruct n. inversion H. compute. trivial.
intros.
destruct n.
inversion H.
simpl.
replace (Ndiv_mod_algo (S n) m) with m.
replace (beq_nat n m) with false.
reflexivity.
apply eq_nat_correct.
intro.
rewrite H0 in H.
apply lt_irrefl in H. contradiction.
symmetry.
apply IHm.
auto with arith.
Qed.

Lemma Ndiv_mod_l1 : n m, n > 0 → Ndiv_mod_algo n (m + n) = Ndiv_mod_algo n m.
Proof.
intros n m. pattern m. apply nat_strong_ind.
intros. simpl.
induction n.
reflexivity.
simpl.
replace (Ndiv_mod_algo (S n) n) with n.
replace (beq_nat n n) with true.
reflexivity. apply beq_nat_refl.
symmetry.
apply Ndiv_mod_l0.
auto with arith.
intros.
induction n.
simpl. reflexivity.
simpl.
replace (Ndiv_mod_algo (S n) (n0+S n)) with (Ndiv_mod_algo (S n) n0).
Focus 2.
symmetry.
apply H.
auto with arith.
auto with arith.
auto.
Qed.

Correctness of divisibility algorithm
Theorem Ndiv_algo_correct : n m, n > 0 → (n | m)Ndiv_algo n m=true.
Proof.
destruct n.
intros.
inversion H.
intro. pattern m.
apply nat_strong_ind.
intros.
compute. trivial.
intros.
unfold Ndiv_algo.
destruct H1.
destruct q.
simpl in H1.
inversion H1.
rewrite mult_succ_l in H1.
rewrite H1.
rewrite Ndiv_mod_l1.
apply H.
apply le_trans with (q×S n+n).
auto with arith.
rewrite plus_comm in H1.
simpl in H1.
apply eq_add_S in H1.
rewrite H1.
rewrite plus_comm.
auto with arith.
auto with arith.
q.
auto.
auto.
Qed.

Lemma Ndiv_mod_algo_rem : n m r, n > 0 → Ndiv_mod_algo n m = rr < n.
Proof.
induction m.
intros.
destruct n. inversion H. compute in H0. rewrite <- H0. auto with arith.
intros.
destruct n. inversion H.
simpl in H0.
assert (Ndiv_mod_algo (S n) m<(S n)).
apply IHm. auto with arith. auto.
apply le_le_S_eq in H1.
destruct H1.
apply le_S_n in H1.
apply le_lt_n_Sm in H1.
apply lt_S_n in H1.
destruct (beq_nat n (Ndiv_mod_algo (S n) m)).
rewrite <- H0. auto with arith.
rewrite <- H0.
apply lt_n_S. auto.
apply eq_add_S in H1.
rewrite H1 in H0.
rewrite <- beq_nat_refl in H0.
rewrite <- H0.
auto with arith.
Qed.

Lemma Ndiv_mod_algo_rem2 : n m r, n > 0 → Ndiv_mod_algo n m = rr m.
Proof.
induction m.
intros.
destruct n; compute in H0; rewrite <- H0; auto with arith.
intros.
simpl in H0.
destruct n. inversion H.
destruct (beq_nat (S n) (S (Ndiv_mod_algo (S n) m))).
rewrite <- H0. auto with arith.
destruct r.
inversion H0.
apply eq_add_S in H0.
apply le_n_S.
apply IHm.
auto.
auto.
Qed.

Completeness of modulus algorithm
Theorem Ndiv_mod_algo_complete : n m r, n > 0 → Ndiv_mod_algo n m = r
(n | m - r).
Proof.
destruct n.
+ intros; inversion H.
+ intro m; pattern m; apply nat_strong_ind.
- intros; compute in H0; rewrite <- H0.
simpl; apply Ndiv_0.
- intros; simpl in H1; case (lt_eq_lt_dec (S n) n0).
intros; destruct s.

{ assert ( d, n0=S n+d) by (apply Nle_plus; auto with arith).
destruct H2; rewrite H2 in H1.
assert (Ndiv_mod_algo (S n) (S n+x)=Ndiv_mod_algo (S n) (x+S n)) by (rewrite plus_comm; auto).
rewrite H3 in H1.
clear H3.
rewrite Ndiv_mod_l1 in H1.
rewrite H2.
replace (S (S n+x)) with (S n+S x).
Focus 2.
auto with arith.
replace (S n+S x-r) with (S n+(S x-r)).
Focus 2.
apply plus_minus.
replace (r+(S n+(S x-r))) with (S n+r+(S x-r)).
Focus 2.
rewrite plus_assoc.
now auto with arith.
assert (S x=r+(S x-r)).
symmetry.
apply le_plus_minus_r.
destruct (beq_nat n (Ndiv_mod_algo (S n) x)).
rewrite <- H1. auto with arith.
destruct r. inversion H1.
apply eq_add_S in H1.
apply le_n_S.
apply Ndiv_mod_algo_rem2 with (S n).
auto with arith.
auto.
rewrite H3.
rewrite plus_assoc.
rewrite minus_plus.
auto.
apply Ndiv_plus_compat.
apply Ndiv_n_n.
apply H.
rewrite plus_Snm_nSm in H2.
apply le_trans with (S x+n).
auto with arith.
rewrite plus_comm.
rewrite <- H2.
auto with arith.
auto with arith.
auto.
auto with arith. }

{
rewrite <- e in H1.
replace (Ndiv_mod_algo (S n) (S n)) with (Ndiv_mod_algo (S n) (0+S n)) in H1.
rewrite Ndiv_mod_l1 in H1.
simpl in H1; destruct n.
{ simpl in H1; rewrite <- H1; rewrite <- e; simpl; 2; ring. }
{ simpl in H1; rewrite <- H1; rewrite e; simpl; rewrite <- minus_n_O; apply Ndiv_n_n. }
{ auto with arith. }
{ simpl. auto. }
}

{
intro;
replace (Ndiv_mod_algo (S n) n0) with n0 in H1.
apply le_le_S_eq in l.
destruct l.
assert (nn0).
intro. rewrite H3 in H2. apply lt_irrefl in H2. auto.
apply eq_nat_correct in H3.
rewrite <- H3 in H1.
rewrite <- H1.
rewrite <- minus_diag_reverse.
apply Ndiv_0.
apply eq_add_S in H2.
rewrite H2 in H1.
rewrite <- beq_nat_refl in H1.
rewrite <- H1.
rewrite <- minus_n_O.
rewrite H2.
apply Ndiv_n_n.
symmetry.
apply Ndiv_mod_l0.
auto. }
Qed.

Completeness of the divisibility algorith
Theorem Ndiv_algo_complete : n m, n>0 → Ndiv_algo n m=true(n | m).
Proof.
intros.
unfold Ndiv_algo in H0.
symmetry in H0.
apply beq_nat_eq in H0.
replace m with (m-0).
apply Ndiv_mod_algo_complete.
auto.
auto.
auto with arith.
Qed.

# Greatest strict divisor

Algorithm to compute the greatest divisor lower than a number
Fixpoint Ngreatest_div_le (n:nat) (p:nat) {struct n}: nat :=
match n with
| 0 | 1 ⇒ 1
| S n
if Ndiv_algo (S n) p then (S n)
else Ngreatest_div_le n p
end.

Algorithm to compute the greatest strict divisor of a number
Definition Ngreatest_div (p:nat) : nat :=
Ngreatest_div_le (pred p) p.

The greatest divisor is a divisor
Lemma Ngreatest_div_le_div : p n, p>1 → (Ngreatest_div_le n p | p).
Proof.
induction n.
intros.
compute. apply Ndiv_1.
intros.
simpl.
destruct n. apply Ndiv_1.
assert(Ndiv_algo (S(S n)) p=true(S(S n)|p)).
intros. apply Ndiv_algo_complete. auto with arith. auto.
destruct (Ndiv_algo (S(S n)) p).
apply H0. auto.
auto.
Qed.

The greatest strict divisor is a divisor
Theorem Ngreatest_div_div : p, p > 1 → (Ngreatest_div p | p).
Proof.
intros.
apply Ngreatest_div_le_div.
auto.
Qed.

The greatest divisor lower than a number is a lower than that number
Theorem Ngreatest_div_le_le : n p, n > 0 → Ngreatest_div_le n p n.
Proof.
intros.
induction n.
inversion H.
simpl.
destruct n.
auto.
destruct (Ndiv_algo (S (S n)) p).
auto.
eapply le_trans.
eapply IHn. auto with arith.
auto with arith.
Qed.

The greatest divisor is a monotonous function
Theorem Ngreatest_div_le_monotone : n n' p,
n n'Ngreatest_div_le n p Ngreatest_div_le n' p.
Proof.
intros.
induction H.
auto.
eapply le_trans.
eexact IHle.
assert (Ndiv_algo (S m) p=trueNgreatest_div_le (S m) p=S m).
intros.
simpl.
destruct m. auto.
rewrite H0. auto.
assert (Ndiv_algo (S m) p=falseNgreatest_div_le (S m) p=Ngreatest_div_le m p).
intros.
simpl.
destruct m. compute. auto.
rewrite H1. auto.
destruct (Ndiv_algo (S m) p).
rewrite H0.
destruct m. compute. auto.
eapply le_trans.
eapply Ngreatest_div_le_le. auto with arith.
auto with arith. auto.
rewrite H1. auto. auto.
Qed.

The greatest divisor is a the greatest divisor
Theorem Ngreatest_div_le_greatest : n p q,
p>1 → q1 → q<pqn(q | p)q Ngreatest_div_le n p.
Proof.
intros.
replace q with (Ngreatest_div_le q p).
apply Ngreatest_div_le_monotone. auto.
destruct q.
inversion H0.
simpl.
destruct q.
auto.
apply Ndiv_algo_correct in H3.
rewrite H3. auto. auto with arith.
Qed.

The greatest strict divisor is a the greatest strict divisor
Theorem Ngreatest_div_greatest : p q,
p>1 → q1 → q<p(q | p)q Ngreatest_div p.
Proof.
intros.
apply Ngreatest_div_le_greatest; auto.
destruct p. inversion H.
simpl. auto with arith.
Qed.

The greatest strict divisor is strict
Theorem Ngreatest_div_lt_p : n, n > 1 → Ngreatest_div n < n.
Proof.
intros.
destruct n.
inversion H.
destruct n.
inversion H. inversion H1.
unfold lt.
apply le_n_S.
unfold Ngreatest_div.
replace (pred(S(S n))) with (S n).
apply Ngreatest_div_le_le.
auto with arith.
auto with arith.
Qed.

The greatest strict divisor is nonzero
Theorem Ngreatest_div_le_1 : n, Ngreatest_div n1.
Proof.
intros.
destruct n.
compute. auto.
destruct n. compute. auto.
apply Ngreatest_div_greatest.
auto with arith.
auto.
auto with arith.
apply Ndiv_1.
Qed.

# Decidability of primality with greatest strict divisor

Implication of greatest strict divisor on primality
Theorem Ngreatest_div_1_prime : p, p > 1 → Ngreatest_div p = 1 → Nprime p.
Proof.
intro.
destruct p.
intros. inversion H.
destruct p.
intros. inversion H. inversion H2.

intros.
split.
auto.
intros.
intro.
apply Ngreatest_div_greatest in H2.
rewrite H0 in H2.
destruct H1.
assert(1<1).
eapply le_trans.
eapply H1. auto.
inversion H4. inversion H6.
auto with arith.
destruct H1.
auto with arith.
destruct H1.
auto with arith.
Qed.

Implication of primality greatest divisor
Theorem Nprime_greatest_div_le_1 : n p, n<pNprime pNgreatest_div_le n p=1.
Proof.
induction n.
intros.
compute. auto.
intros.
simpl.
destruct n.
auto.
assert(~(Ndiv_algo (S (S n)) p=true)).
intro.
destruct H0.
apply H2 with (S(S n)).
split.
auto with arith. auto.
apply Ndiv_algo_complete.
auto with arith. auto.
destruct (Ndiv_algo (S (S n)) p).
apply IHn.
auto with arith.
auto.
Qed.

Implication of primality greatest strict divisor
Theorem Nprime_greatest_div_1 : p, Nprime pNgreatest_div p=1.
Proof.
intros.
apply Nprime_greatest_div_le_1.
destruct H.
inversion H;
auto with arith. auto.
Qed.

# Lowest strict divisor

Algorithm to compute the lowest divisor greater than a number
Fixpoint Nleast_div_ge (n p:nat) {struct n} : nat :=
match n with
| 0 ⇒ p
| S n
if Ndiv_algo (p-S n) p then p-S n
else Nleast_div_ge n p
end.

Algorithm to compute lowest strict divisor
Definition Nleast_div p := Nleast_div_ge (p-2) p.

Lowest divisor is a divisor
Lemma Nleast_div_ge_div : p n, p>1 → n < p(Nleast_div_ge n p | p).
Proof.
induction n.
intros.
compute. apply Ndiv_n_n.
intros.
simpl.
assert (Ndiv_algo (p-S n) p=true(p-S n|p)).
apply Ndiv_algo_complete.
unfold gt.
apply (minus_le_compat_r (S (S n)) p (S n)) in H0.
rewrite <- minus_Sn_m in H0.
rewrite <- minus_n_n in H0.
eapply le_trans.
eapply H0. auto. auto.
destruct (Ndiv_algo (p-S n) p).
apply H1. auto.
apply IHn. auto.
auto with arith.
Qed.

Lowest divisor is usually greater than 1
Theorem Nleast_div_ge_gt_1 : n p, p > 1 → S n < p → 1 < Nleast_div_ge n p.
Proof.
induction n.
intros.
compute. auto.
intros.
simpl.
destruct (Ndiv_algo (p-S n) p).
apply (minus_le_compat_r (S(S(S n))) p (S n)) in H0.
rewrite <- minus_Sn_m in H0.
rewrite <- minus_Sn_m in H0.
rewrite <- minus_n_n in H0.
auto. auto. auto.
apply IHn.
auto. auto with arith.
Qed.

Lowest strict divisor is greater than 1
Theorem Nleast_div_gt_1 : p, p > 1 → 1 < Nleast_div p.
Proof.
intros.
apply Nleast_div_ge_gt_1.
auto.
unfold lt.
assert(p2).
auto with arith.
apply Nle_plus in H0.
destruct H0.
rewrite H0.
rewrite minus_plus.
auto with arith.
Qed.

Lowest strict divisor is a divisor
Theorem Nleast_div_div : p, p>1 → (Nleast_div p | p).
Proof.
intros.
apply Nleast_div_ge_div.
auto.
auto with arith.
Qed.

Lowest divisor greater than a number is greater than that number
Theorem Nleast_div_ge_ge : n p, n < pNleast_div_ge n p p - n.
Proof.
induction n.
intros.
simpl.
rewrite <- minus_n_O.
auto.
intros.
simpl.
destruct (Ndiv_algo (p-S n) p).
auto.
unfold ge.
apply le_trans with (p-n).
apply minus_le_compat_l.
auto.
apply IHn. auto with arith.
Qed.

Lowest divisor is a monotonous function
Theorem Nleast_div_ge_monotone : n n' p,
n n'n' < pNleast_div_ge n p Nleast_div_ge n' p.
Proof.
intros.
induction H.
auto.
simpl.
destruct (Ndiv_algo (p-S m) p).
apply le_trans with (p-m).
apply minus_le_compat_l.
auto.
apply le_trans with (p-n).
apply minus_le_compat_l.
auto.
apply Nleast_div_ge_ge.
apply le_trans with (S m).
auto with arith.
auto with arith.
apply IHle.
auto with arith.
Qed.

Lowest divisor is lowest divisor
Theorem Nleast_div_ge_least : n p q,
p > 1 → q 1 → q < pn < pq p-n(q | p)Nleast_div_ge n p q.
Proof.
intros.
replace q with (Nleast_div_ge (p-q) p).
apply Nleast_div_ge_monotone.
unfold ge in H3.
destruct (le_dec n p).
apply (plus_le_compat_l (p-n) q n) in H3.
rewrite le_plus_minus_r in H3.
apply (minus_le_compat_r p (n+q) q) in H3.
rewrite plus_comm in H3.
rewrite minus_plus in H3.
auto.
auto.
apply le_trans with p.
apply le_minus.
auto.
auto.

destruct H1.
rewrite <- minus_Sn_m.
rewrite <- minus_n_n.
simpl. rewrite <- minus_n_O.
apply Ndiv_algo_correct in H4.
rewrite H4. auto. auto. auto.

rewrite <- minus_Sn_m.
simpl.
apply Ndiv_algo_correct in H4.
assert(qm).
auto with arith.
apply Nle_plus in H5.
destruct H5.
rewrite H5.
rewrite minus_plus.
rewrite plus_comm.
rewrite minus_plus.
rewrite H5 in H4.
rewrite plus_comm.
rewrite H4.
auto. auto. auto with arith.
Qed.

Lowest strict divisor is lowest divisor
Theorem Nleast_div_least : p q,
p > 1 → q > 1 → q < p(q | p)Nleast_div p q.
Proof.
intros.
apply Nleast_div_ge_least.
auto. auto with arith. auto. auto with arith.
apply Nle_plus in H.
destruct H.
rewrite H.
rewrite minus_plus.
rewrite plus_comm.
rewrite minus_plus.
auto.
auto.
Qed.

# Decidability of primality with lowest strict divisor

Implication of lowest strict divisor on primality
Theorem Nleast_div_p_prime : p, p > 1 → Nleast_div p = pNprime p.
Proof.
intros.
destruct p.
inversion H.
split.
auto.
intros.
destruct H1.
intro.
apply Nleast_div_least in H3.
rewrite H0 in H3.
assert(n<n).
apply le_trans with (S p).
auto. auto.
apply lt_irrefl in H4. auto.
auto.
auto.
auto.
Qed.

Implication of primality on lowest divisor
Theorem Nprime_least_div_ge_p : n p, S n < pNprime pNleast_div_ge n p = p.
induction n.
intros.
compute. auto.
intros.
destruct H0.
apply le_le_S_eq in H.
destruct H.
simpl.
assert(¬(p-S n|p)).
apply H1.
split.
apply (minus_le_compat_r (S(S(S(S n)))) p (S n)) in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_n_n in H.
auto with arith.
auto.
auto.
auto with arith.
apply lt_minus.
apply le_trans with (S(S(S n))).
auto with arith. auto.
auto with arith.
auto with arith.
assert (¬Ndiv_algo (p-S n) p=true).
intro.
apply H1 with (p-S n).
split.
apply (minus_le_compat_r (S(S(S(S n)))) p (S n)) in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_n_n in H.
auto with arith.
auto.
auto.
auto.
apply lt_minus.
apply le_trans with (S(S(S(S n)))).
auto. auto. auto with arith.
apply Ndiv_algo_complete.
unfold gt.
apply (minus_le_compat_r (S(S(S(S n)))) p (S n)) in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_Sn_m in H.
rewrite <- minus_n_n in H.
apply le_trans with 3. auto. auto. auto. auto. auto. auto. auto with arith.

destruct (Ndiv_algo (p-S n) p).
apply IHn.
apply le_trans with (S(S(S(S n)))).
auto. auto.
split. auto. auto.

destruct p. inversion H.
destruct p. inversion H.
destruct p. inversion H.
do 3 apply eq_add_S in H.
rewrite H.
unfold Nleast_div_ge.
rewrite <- minus_Sn_m.
rewrite <- minus_Sn_m.
rewrite <- minus_n_n.
assert(~(Ndiv_algo 2 (S(S(S p)))=true)).
intro.
apply H1 with 2.
split. auto. auto with arith.
apply Ndiv_algo_complete. auto. auto.
destruct (Ndiv_algo 2 (S(S(S p)))).
fold Nleast_div_ge.
rewrite <- H.
apply IHn.
auto.
split. auto with arith.
rewrite H.
auto.
auto.
auto.
Qed.

Implication of primality on lowest strict divisor
Theorem Nprime_least_div_p : p, Nprime pNleast_div p = p.
Proof.
intros.
apply Nprime_least_div_ge_p.
destruct p.
apply Nnot_prime_0 in H. contradiction.
destruct p.
apply Nnot_prime_1 in H. contradiction.
rewrite minus_Sn_m.
apply le_trans with (S (S p)).
apply lt_n_S.
auto with arith. auto. auto with arith.
auto.
Qed.

Lowest strict divisor is prime
Theorem Nleast_div_prime : p, p>1 → Nprime (Nleast_div p).
Proof.
intros.
split.
apply Nleast_div_gt_1.
auto.
intros.
intro.
destruct H0.
assert((n|p)).
apply Ndiv_trans with (Nleast_div p).
auto.
apply Nleast_div_div.
auto with arith.
apply Nleast_div_least in H3.
apply lt_irrefl with (Nleast_div p).
apply le_trans with (S n).
auto with arith.
auto.
auto with arith.
auto.
apply le_trans with (Nleast_div p).
auto.
apply Ndiv_le.
destruct p. inversion H.
auto with arith.
apply Nleast_div_div.
auto with arith.
Qed.

Lowest strict divisor is greater than 1
Theorem Nleast_div_ge_2 : n, n > 1 → Nleast_div n 2.
Proof.
intros.
assert(Nprime (Nleast_div n)).
apply Nleast_div_prime.
auto.
assert(0Nleast_div n).
auto with arith.
apply le_le_S_eq in H1.
destruct H1.
apply le_le_S_eq in H1.
destruct H1.
auto.
rewrite <- H1 in H0.
apply Nnot_prime_1 in H0. contradiction.
rewrite <- H1 in H0.
apply Nnot_prime_0 in H0. contradiction.
Qed.

Implication of lowest strict divisor on not primality
Theorem Nleast_div_lt_p_not_prime : n, n > 2 → (Nleast_div n) < n~(Nprime n).
Proof.
intros.
intro.
assert((Nleast_div n|n)).
apply Nleast_div_div.
auto with arith.
destruct H2.
destruct q.
rewrite mult_0_l in H2.
rewrite H2 in H.
inversion H.
destruct q.
rewrite mult_1_l in H2.
rewrite <- H2 in H0.
apply lt_irrefl in H0.
auto.
apply (Ncomposed_not_prime (S(S q)) (Nleast_div n)).
auto with arith.
apply Nleast_div_gt_1.
auto with arith.
rewrite H2 in H1. auto.
Qed.

Every number has a prime divisor
Theorem Nhas_prime_divisor : n, n > 1 → p, Nprime p (p | n).
Proof.
intros.
(Nleast_div n).
split.
apply Nleast_div_prime.
auto.
apply Nleast_div_div.
auto with arith.
Qed.

# Gauss theorem (prime formulation)

Theorem Ngauss_prime : a b c, (a | b × c)Nprime a(a | c) (a | b).
Proof.
intros.
destruct a.
apply Nnot_prime_0 in H0. contradiction.

assert(Ndiv_algo (S(a)) b=true((S(a))|b)).
intro. apply Ndiv_algo_complete. auto.
auto with arith. auto.
assert(Ndiv_algo (S a) b=falseNrel_prime (S a) b).
intro.
assert(¬(S a|b)).
intro.
apply Ndiv_algo_correct in H3. rewrite H3 in H2. inversion H2.
auto with arith.
intro.
intros.
destruct n.
destruct H4. rewrite mult_0_r in H4. inversion H4.
destruct n.
auto.
destruct H0.
apply H6 in H4.
split.
auto with arith.
apply Ndiv_le in H4.
apply le_le_S_eq in H4.
destruct H4.
auto.
rewrite H4 in H5.
apply H3 in H5.
auto with arith.
destruct (Ndiv_algo (S a) b).
right.
apply H1.
auto.
left.
apply Ngauss with b.
apply H.
apply H2.
auto.
Qed.

# Compatibility of coprimality with multiplication

Theorem Nrel_prime_mult_compat : p n m,
Nrel_prime p nNrel_prime p mNrel_prime p (n × m).
Proof.
intros.
intro.
intros.
destruct n0.
destruct H1.
rewrite mult_0_r in H1.
rewrite H1 in H.
destruct H2.
rewrite mult_0_r in H2.
apply mult_is_O in H2.
destruct H2.
rewrite H2 in H.
apply H.
apply Ndiv_n_n.
apply Ndiv_n_n.
rewrite H1 in H0.
rewrite H2 in H0.
apply H0.
apply Ndiv_n_n.
apply Ndiv_n_n.
destruct n0.
auto.

assert( pn0, Nprime pn0 (pn0|(S(S n0)))).
apply Nhas_prime_divisor.
auto with arith.
destruct H3.
destruct H3.
assert((x|n×m)).
eapply Ndiv_trans.
eapply H4.
apply H2.
apply Ngauss_prime in H5.
assert(x=1).
destruct H5.
apply H0.
eapply Ndiv_trans. eapply H4. apply H1.
apply H5.
apply H.
eapply Ndiv_trans. eapply H4. apply H1.
apply H5.
rewrite H6 in H3.
apply Nnot_prime_1 in H3.
auto.
Qed.

# Primality results

Not prime implies composed
Theorem Nnot_prime_composed : n,
n > 2 → ~(Nprime n) p, q, p > 1 q > 1 n = p × q.
Proof.
intros.
(Nleast_div n).
assert(Nleast_div n|n).
apply Nleast_div_div.
auto with arith.
destruct H1.
q.
split.
apply Nleast_div_gt_1. auto with arith.
split.
destruct q.
rewrite mult_0_l in H1.
rewrite H1 in H.
inversion H.
destruct q.
rewrite mult_1_l in H1.
symmetry in H1.
apply Nleast_div_p_prime in H1.
apply H0 in H1. contradiction.
auto with arith.
auto with arith.
rewrite mult_comm. auto.
Qed.

A number if either prime or not prime
Theorem Nprime_or_not_prime : n, (Nprime n) (~(Nprime n)).
Proof.
intros.
destruct n.
right. apply Nnot_prime_0.
destruct n.
right. apply Nnot_prime_1.
destruct n.
left.
apply Nprime_intro.
auto with arith.
intros.
destruct H.
inversion H.
rewrite H1 in H0.
apply lt_irrefl in H0. contradiction.
rewrite <- H2 in H0.
assert(2<2).
apply le_trans with (S m).
auto with arith. auto with arith.
apply lt_irrefl in H3. contradiction.
assert(beq_nat (Nleast_div (S(S(S n)))) (S(S(S n)))=trueNprime (S(S(S n)))).
intros.
apply Nleast_div_p_prime.
auto with arith.
apply beq_nat_true.
auto.
assert(beq_nat (Nleast_div (S(S(S n)))) (S(S(S n)))=false¬Nprime (S(S(S n)))).
intros.
assert(Nleast_div (S(S(S n)))<>(S(S(S n)))).
apply beq_nat_false.
auto.
apply not_eq in H1.
destruct H1.
apply Nleast_div_lt_p_not_prime.
auto with arith.
auto.
assert(Nleast_div (S(S(S n)))S(S(S n))).
apply Ndiv_le.
auto with arith.
apply Nleast_div_div.
auto with arith.
assert(S(S(S n))<S(S(S n))).
eapply le_trans.
eapply H1.
apply H2.
apply lt_irrefl in H3.
intro. auto.

destruct (beq_nat (Nleast_div (S (S (S n)))) (S (S (S n)))).
left. auto.
right. auto.
Qed.

A number is either prime or composed
Theorem Nprime_or_composed : n,
n > 2 → (Nprime n) ( p, q, p > 1 q > 1 n=p × q).
Proof.
intros.
assert(Nprime n ¬Nprime n).
apply Nprime_or_not_prime.
destruct H0.
left. auto.
right.
apply Nnot_prime_composed.
auto. auto.
Qed.

# Relation between lowest strict divisor and greatest strict divisor

Theorem Ngreatest_least_div_relation : n, n > 2 → (Ngreatest_div n) × (Nleast_div n)=n.
Proof.
intros.
assert(Nprime n ¬Nprime n).
apply Nprime_or_not_prime.
destruct H0.
replace (Ngreatest_div n) with 1.
replace (Nleast_div n) with n.
ring.
symmetry.
apply Nprime_least_div_p. auto.
symmetry.
apply Nprime_greatest_div_1. auto.

assert(Q:¬Nprime n).
auto. clear H0.
assert((Ngreatest_div n)*(Nleast_div n)n).
assert((Ngreatest_div n)|n).
apply Ngreatest_div_div. auto with arith.
destruct H0.
assert(q|n).
(Ngreatest_div n).
rewrite mult_comm. auto.
apply Nleast_div_least in H1.
rewrite H0 at 3.
rewrite mult_comm.
apply mult_le_compat_r.
auto.
auto with arith.
destruct q.
rewrite mult_0_l in H0. rewrite H0 in H. inversion H.
destruct q.
rewrite mult_1_l in H0.
assert(Ngreatest_div n<n).
apply Ngreatest_div_lt_p.
auto with arith.
rewrite <- H0 in H2 at 1.
apply lt_irrefl in H2.
auto with arith.
assert(qn).
apply Ndiv_le; auto. destruct n. inversion H. auto with arith.
apply le_le_S_eq in H2.
destruct H2.
auto.
rewrite H2 in H0.
destruct n.
inversion H.
assert(1Ngreatest_div (S n)).
apply Ngreatest_div_le_1.
apply le_le_S_eq in H3.
destruct H3.
replace q with (q×1).
rewrite H0.
rewrite H2.
apply mult_S_lt_compat_l.
auto. ring.
symmetry in H3.
apply Ngreatest_div_1_prime in H3.
apply Q in H3. contradiction.
auto with arith.

assert((Ngreatest_div n)*(Nleast_div n)n).
assert((Nleast_div n)|n).
apply Nleast_div_div. auto with arith.
destruct H1.
assert(q|n).
(Nleast_div n).
rewrite mult_comm. auto.
apply Ngreatest_div_greatest in H2.
unfold ge.
rewrite H1 at 1.
apply mult_le_compat_r.
auto.
auto with arith.
destruct q.
rewrite mult_0_l in H1.
rewrite H1 in H. inversion H.
auto with arith.
apply Ndiv_le in H2.
apply le_le_S_eq in H2.
destruct H2.
auto.
rewrite H2 in H1.
assert(Nleast_div n2).
apply Nleast_div_ge_2.
destruct n. inversion H.
auto with arith.
replace q with (q×1).
rewrite H1.
rewrite H2.
destruct n.
inversion H.
apply mult_S_lt_compat_l.
auto. ring.
destruct n.
inversion H.
auto with arith.

apply le_antisym; auto.
Qed.