(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


(**
   prime.
   The primality predicate.
 
   @author Olga Caprotti and Martijn Oostdijk
   @version $Revision$
*)

Require Import ZArith.
Require Import Wf_nat.

Require Import lemmas.
Require Import natZ.
Require Import dec.
Require Import divides.
Require Import modulo.
Require Import list.


(** * Primality on nat *)

Definition Prime (n : nat) : Prop :=
  n > 1 /\ (forall q : nat, Divides q n -> q = 1 \/ q = n).

(** Prime with bounded all quantifier. *)

Definition bPrime (n : nat) :=
  n > 1 /\ (forall q : nat, q < S n -> Divides q n -> q = 1 \/ q = n).

Lemma primebprime : forall n : nat, Prime n <-> bPrime n.
Proof.
(* Goal: forall n : nat, iff (Prime n) (bPrime n) *)
   unfold Prime, bPrime in |- *.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   intro. elim H.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros.
(* Goal: False *)
   apply H1.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   intro. elim H.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros.
(* Goal: False *)
   apply H1.
(* Goal: lt x N *)
(* Goal: gt x (S O) *)
(* Goal: not (Prime x) *)
(* Goal: gt N (S O) *)
(* Goal: not (Prime N) *)
   unfold lt in |- *.
(* Goal: le (S q) (S n) *)
(* Goal: Divides q n *)
   apply le_n_S.
(* Goal: le q n *)
(* Goal: Divides q n *)
   apply div_le.
(* Goal: alllist Z ZPrime t *)
   apply lt_trans with 1. apply lt_O_Sn. assumption.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: alllist Z ZPrime t *)
   assumption.
Qed.

(** Prime is decidable. *)

Lemma bprimedec : forall n : nat, bPrime n \/ ~ bPrime n.
Proof.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   unfold bPrime in |- *. intros.
(* Goal: or (and (lt (S O) n0) (Divides n0 (S (S n2)))) (not (and (lt (S O) n0) (Divides n0 (S (S n2))))) *)
   apply anddec.
(* Goal: or (gt n (S O)) (not (gt n (S O))) *)
(* Goal: or (forall (q : nat) (_ : lt q (S n)) (_ : Divides q n), or (@eq nat q (S O)) (@eq nat q n)) (not (forall (q : nat) (_ : lt q (S n)) (_ : Divides q n), or (@eq nat q (S O)) (@eq nat q n))) *)
   apply gtdec.
(* Goal: or (forall (q : nat) (_ : lt q (S n)) (_ : Divides q n), or (@eq nat q (S O)) (@eq nat q n)) (not (forall (q : nat) (_ : lt q (S n)) (_ : Divides q n), or (@eq nat q (S O)) (@eq nat q n))) *)
   apply (alldec (fun q : nat => Divides q n -> q = 1 \/ q = n) (S n)).
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros.
(* Goal: or (forall _ : Divides n0 n, or (@eq nat n0 (S O)) (@eq nat n0 n)) (not (forall _ : Divides n0 n, or (@eq nat n0 (S O)) (@eq nat n0 n))) *)
   apply impdec.
(* Goal: or (Divides n0 (S (S n2))) (not (Divides n0 (S (S n2)))) *)
   apply divdec.
(* Goal: or (or (@eq nat n0 (S O)) (@eq nat n0 n)) (not (or (@eq nat n0 (S O)) (@eq nat n0 n))) *)
   apply ordec.
(* Goal: or (@eq nat n0 n) (not (@eq nat n0 n)) *)
   apply eqdec.
(* Goal: or (@eq nat n0 n) (not (@eq nat n0 n)) *)
   apply eqdec.
Qed.

Lemma primedec : forall n : nat, Prime n \/ ~ Prime n.
Proof.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   intro. elim (primebprime n).
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros. elim (bprimedec n).
(* Goal: forall _ : @eq Z (Z.of_nat q) (Zpos xH), or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
(* Goal: forall _ : @eq Z (Z.of_nat q) n, or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
(* Goal: Z.ge (Z.of_nat q) Z0 *)
(* Goal: ZDivides (Z.of_nat q) n *)
   left. apply (H0 H1).
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   right. intro. apply H1. apply (H H2).
Qed.

(** Non-primes n>1 have non-trivial divisors. *)

Lemma nonprime_witness :
 forall n : nat,
 n > 1 -> ~ Prime n -> exists d : nat, 1 < d /\ d < n /\ Divides d n.
Proof.
(* Goal: forall (n : nat) (_ : gt n (S O)) (_ : not (Prime n)), @ex nat (fun d : nat => and (lt (S O) d) (and (lt d n) (Divides d n))) *)
   intro n. case n.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   intro. elim (lt_n_O 1). assumption.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   intro n1. case n1. intro. elim (lt_irrefl 1). assumption.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intro n2. intros.
   elim
    (decDeMorgan (S (S n2)) (fun d : nat => 1 < d /\ Divides d (S (S n2)))).
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros. elim H2. intros.
(* Goal: @ex nat (fun d : nat => and (lt (S O) d) (and (le (Init.Nat.mul d d) N) (and (Divides d N) (Prime d)))) *)
(* Goal: forall _ : not (Prime x), @ex nat (fun d : nat => and (lt (S O) d) (and (le (Init.Nat.mul d d) N) (and (Divides d N) (Prime d)))) *)
(* Goal: gt N (S O) *)
(* Goal: not (Prime N) *)
   split with x.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H3. intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H5. intros.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intro. apply H0. unfold Prime in |- *. split. assumption.
(* Goal: forall (q : nat) (_ : Prime q) (_ : Divides q (S (S O))), gt (Init.Nat.mul q q) (S (S O)) *)
   intro q. case q.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   intro. unfold Divides in H4. elim H4. simpl in |- *. intros. discriminate H5.
(* Goal: forall _ : @eq Z (Z.of_nat q) (Zpos xH), or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
(* Goal: forall _ : @eq Z (Z.of_nat q) n, or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
(* Goal: Z.ge (Z.of_nat q) Z0 *)
(* Goal: ZDivides (Z.of_nat q) n *)
   intro q1. case q1. left. reflexivity.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intro q2. intros. right.
(* Goal: @eq nat (S (S q2)) (S (S n2)) *)
(* Goal: forall n : nat, or (and (lt (S O) n) (Divides n (S (S n2)))) (not (and (lt (S O) n) (Divides n (S (S n2))))) *)
   elim (le_lt_or_eq (S (S q2)) (S (S n2))).
(* Goal: alllist Z ZPrime t *)
   intros. elim (H3 (S (S q2))). assumption.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split. apply lt_n_S. apply lt_O_Sn. assumption.
(* Goal: alllist Z ZPrime t *)
   intros. assumption.
(* Goal: alllist Z ZPrime t *)
   apply div_le1. assumption.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros. apply anddec. apply ltdec. apply divdec.
Qed.

Lemma nonprime_sqrwitness :
 forall n : nat,
 n > 1 -> ~ Prime n -> exists d : nat, 1 < d /\ d * d <= n /\ Divides d n.
Proof.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros. elim (nonprime_witness n).
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intro d. intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim (sqrdivbound n d). intro d'. intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H2. intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H4. intros.
(* Goal: Prime n *)
(* Goal: gt n (S O) *)
(* Goal: not (Prime n) *)
   elim H6.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   intro. split with d'.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split. rewrite H7. elim H1. tauto.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split. assumption.
(* Goal: lt d (Init.Nat.mul d d') *)
(* Goal: and (le (Init.Nat.mul d' d') n) (Divides d' n) *)
(* Goal: Divides d n *)
(* Goal: gt n (S O) *)
(* Goal: not (Prime n) *)
   rewrite H7. elim H1. tauto.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intro. split with d'. split. apply (lt_n_nm_m_gt_1 d d').
(* Goal: lt d (Init.Nat.mul d d') *)
(* Goal: and (le (Init.Nat.mul d' d') n) (Divides d' n) *)
(* Goal: Divides d n *)
(* Goal: gt n (S O) *)
(* Goal: not (Prime n) *)
   rewrite H7. elim H1. tauto.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split. assumption.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: @ex nat (fun d : nat => and (lt (S O) d) (and (le (Init.Nat.mul d d) N) (and (Divides d N) (Prime d)))) *)
(* Goal: gt N (S O) *)
(* Goal: not (Prime N) *)
   elim H1. tauto.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: alllist Z ZPrime t *)
   assumption.
Qed.

(** Non-primes n>1 have prime-divisors. *)

Theorem nonprime_primewitness :
 forall n : nat,
 n > 1 ->
 ~ Prime n -> exists d : nat, 1 < d /\ d * d <= n /\ Divides d n /\ Prime d.
Proof.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   intro. apply (lt_wf_ind n).
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros N IH. intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim (nonprime_sqrwitness N). intro x. intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H1. intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H3. intros.
(* Goal: @ex nat (fun d : nat => and (lt (S O) d) (and (le (Init.Nat.mul d d) N) (and (Divides d N) (Prime d)))) *)
(* Goal: gt N (S O) *)
(* Goal: not (Prime N) *)
   elim (primedec x).
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros.
(* Goal: @ex nat (fun d : nat => and (lt (S O) d) (and (le (Init.Nat.mul d d) N) (and (Divides d N) (Prime d)))) *)
(* Goal: forall _ : not (Prime x), @ex nat (fun d : nat => and (lt (S O) d) (and (le (Init.Nat.mul d d) N) (and (Divides d N) (Prime d)))) *)
(* Goal: gt N (S O) *)
(* Goal: not (Prime N) *)
   split with x.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split. assumption.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split. assumption.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split. assumption.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros. elim (IH x). intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H7. intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H9. intros.
(* Goal: @ex nat (fun d : nat => and (lt (S O) d) (and (le (Init.Nat.mul d d) N) (and (Divides d N) (Prime d)))) *)
(* Goal: lt x N *)
(* Goal: gt x (S O) *)
(* Goal: not (Prime x) *)
(* Goal: gt N (S O) *)
(* Goal: not (Prime N) *)
   elim H11.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros.
(* Goal: @ex nat (fun d : nat => and (lt (S O) d) (and (le (Init.Nat.mul d d) N) (and (Divides d N) (Prime d)))) *)
(* Goal: lt x N *)
(* Goal: gt x (S O) *)
(* Goal: not (Prime x) *)
(* Goal: gt N (S O) *)
(* Goal: not (Prime N) *)
   split with x0.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split. assumption.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split. apply le_trans with (x * x).
(* Goal: alllist Z ZPrime t *)
   apply le_trans with x. assumption. apply le_n_nn. assumption.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split. apply div_trans with x. assumption. assumption.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: lt x N *)
(* Goal: gt x (S O) *)
(* Goal: not (Prime x) *)
(* Goal: gt N (S O) *)
(* Goal: not (Prime N) *)
   unfold lt in |- *. apply le_trans with (x * x).
(* Goal: alllist Z ZPrime t *)
   change (x < x * x) in |- *. apply sqr_ascend. assumption.
(* Goal: alllist Z ZPrime t *)
   assumption. assumption. assumption. assumption. assumption.
Qed.

(** Prime(n) if all prime divisors > sqrt(n). *)

Theorem primepropdiv :
 forall n : nat,
 n > 1 -> (forall q : nat, Prime q -> Divides q n -> q * q > n) -> Prime n.
Proof.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros. elim (primedec n).
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   intro. assumption.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros. elim (nonprime_primewitness n).
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H2. intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H4. intros.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H6. intros.
(* Goal: Prime n *)
(* Goal: gt n (S O) *)
(* Goal: not (Prime n) *)
   elim (le_not_lt (x * x) n).
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: alllist Z ZPrime t *)
   unfold gt in H0. apply H0. assumption. assumption.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: alllist Z ZPrime t *)
   assumption.
Qed.

Lemma primediv1p : forall p n : nat, Prime p -> Divides n p -> n = 1 \/ n = p.
Proof.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   unfold Prime in H. elim H. intros.
(* Goal: alllist Z ZPrime t *)
   apply (H2 n). assumption.
Qed.

(** Two is a prime. *)

Lemma prime2 : Prime 2.
Proof.
(* Goal: Prime (S (S O)) *)
   apply primepropdiv.
(* Goal: gt (S (S (S (S O)))) (S (S O)) *)
(* Goal: forall (n : nat) (_ : Prime (S (S (S n)))) (_ : Divides (S (S (S n))) (S (S O))), gt (Init.Nat.mul (S (S (S n))) (S (S (S n)))) (S (S O)) *)
   auto.
(* Goal: forall (q : nat) (_ : Prime q) (_ : Divides q (S (S O))), gt (Init.Nat.mul q q) (S (S O)) *)
   intro q. case q.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   intros. elim H. intro.
(* Goal: alllist Z ZPrime t *)
   elim (lt_n_O 1). assumption.
(* Goal: forall (n : nat) (_ : Prime (S n)) (_ : Divides (S n) (S (S O))), gt (Init.Nat.mul (S n) (S n)) (S (S O)) *)
   intro q1. case q1.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   intros. elim H. intro.
(* Goal: alllist Z ZPrime t *)
   elim (lt_irrefl 1). assumption.
(* Goal: forall (n : nat) (_ : Prime (S (S n))) (_ : Divides (S (S n)) (S (S O))), gt (Init.Nat.mul (S (S n)) (S (S n))) (S (S O)) *)
   intro q2. case q2.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   simpl in |- *. intros. auto.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intro q3. simpl in |- *. intros.
(* Goal: gt (S (S (S (Init.Nat.add q3 (S (S (S (Init.Nat.add q3 (S (S (S (Init.Nat.add q3 (Init.Nat.mul q3 (S (S (S q3)))))))))))))))) (S (S O)) *)
   repeat apply gt_n_S. apply gt_Sn_O.
Qed.

(** * Primality on Z *)

(** ZPrime, just like Prime but uses only Z. *)

Definition ZPrime (n : Z) : Prop :=
  (n > 1)%Z /\ (forall q : Z, (q >= 0)%Z -> ZDivides q n -> q = 1%Z \/ q = n).

Lemma primezprime : forall n : nat, Prime n -> ZPrime (Z_of_nat n).
Proof.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   unfold Prime, ZPrime in |- *. intros.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H. intros. split.
(* Goal: Z.gt (Z.of_nat n) (Zpos xH) *)
(* Goal: forall (q : Z) (_ : Z.ge q Z0) (_ : ZDivides q (Z.of_nat n)), or (@eq Z q (Zpos xH)) (@eq Z q (Z.of_nat n)) *)
   change (Z_of_nat n > Z_of_nat 1)%Z in |- *.
(* Goal: alllist Z ZPrime t *)
   apply Znat.inj_gt. assumption.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros. elim (H1 (Zabs_nat q)).
(* Goal: forall _ : @eq Z (Z.of_nat q) (Zpos xH), or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
(* Goal: forall _ : @eq Z (Z.of_nat q) n, or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
(* Goal: Z.ge (Z.of_nat q) Z0 *)
(* Goal: ZDivides (Z.of_nat q) n *)
   left. rewrite <- (inj_abs_pos q). rewrite H4.
(* Goal: alllist Z ZPrime t *)
   simpl in |- *. reflexivity. assumption.
(* Goal: forall _ : @eq Z (Z.of_nat q) n, or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
(* Goal: Z.ge (Z.of_nat q) Z0 *)
(* Goal: ZDivides (Z.of_nat q) n *)
   right. rewrite <- (inj_abs_pos q). rewrite H4.
(* Goal: alllist Z ZPrime t *)
   reflexivity. assumption.
(* Goal: Divides (Z.abs_nat q) n *)
   rewrite <- (abs_inj n).
(* Goal: alllist Z ZPrime t *)
   apply zdivdiv. assumption.
Qed.

Lemma zprimeprime : forall n : Z, ZPrime n -> Prime (Zabs_nat n).
Proof.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   unfold ZPrime, Prime in |- *. intros.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H. intros. split.
(* Goal: gt (Z.abs_nat n) (S O) *)
(* Goal: forall (q : nat) (_ : Divides q (Z.abs_nat n)), or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
   change (Zabs_nat n > Zabs_nat 1) in |- *.
(* Goal: gt (Z.abs_nat n) (Z.abs_nat (Zpos xH)) *)
(* Goal: forall (q : nat) (_ : Divides q (Z.abs_nat n)), or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
   apply gtzgt.
(* Goal: Z.le Z0 h *)
(* Goal: alllist Z (fun x : Z => Z.ge x Z0) t *)
   apply Zle_trans with 1%Z.
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: alllist Z ZPrime t *)
   apply Zlt_le_weak. apply Zgt_lt. assumption.
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: alllist Z ZPrime t *)
   assumption.
(* Goal: forall (_ : ZPrime h) (_ : alllist Z ZPrime t), and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   intros. elim (H1 (Z_of_nat q)).
(* Goal: forall _ : @eq Z (Z.of_nat q) (Zpos xH), or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
(* Goal: forall _ : @eq Z (Z.of_nat q) n, or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
(* Goal: Z.ge (Z.of_nat q) Z0 *)
(* Goal: ZDivides (Z.of_nat q) n *)
   left. rewrite <- (abs_inj q). rewrite H3.
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   simpl in |- *. reflexivity.
(* Goal: forall _ : @eq Z (Z.of_nat q) n, or (@eq nat q (S O)) (@eq nat q (Z.abs_nat n)) *)
(* Goal: Z.ge (Z.of_nat q) Z0 *)
(* Goal: ZDivides (Z.of_nat q) n *)
   right. rewrite <- (abs_inj q). rewrite H3.
(* Goal: @eq nat (Z.abs_nat n) (Z.abs_nat n) *)
(* Goal: Z.ge (Z.of_nat q) Z0 *)
(* Goal: ZDivides (Z.of_nat q) n *)
   reflexivity. apply nat_ge_0.
(* Goal: alllist Z ZPrime t *)
   apply divzdiv. rewrite abs_inj. assumption.
Qed.

Lemma zprime2 : ZPrime 2.
Proof.
(* Goal: ZPrime (Zpos (xO xH)) *)
   change (ZPrime (Z_of_nat 2)) in |- *.
(* Goal: ZPrime (Z.of_nat h) *)
(* Goal: alllist Z ZPrime (map nat Z Z.of_nat t) *)
   apply primezprime.
(* Goal: Prime (S (S O)) *)
   exact prime2.
Qed.

Lemma zprime2a : ZPrime 2.
Proof.
(* Goal: ZPrime (Zpos (xO xH)) *)
   exact zprime2.
Qed.

(** All numbers in natlist are prime. *)

Definition allPrime : natlist -> Prop := alllist nat Prime.

Definition allZPrime : Zlist -> Prop := alllist Z ZPrime.

Lemma allzprimeallpos : forall l : Zlist, allZPrime l -> allPos l.
Proof.
(* Goal: forall (l : Zlist) (_ : allZPrime l), allPos l *)
   unfold allZPrime, allPos in |- *.
(* Goal: forall (l : Zlist) (_ : alllist Z ZPrime l), alllist nat Prime (map Z nat Z.abs_nat l) *)
   simple induction l.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   simpl in |- *. intro. assumption.
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   simpl in |- *. intros h t IH H.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   elim H. intros. elim H0. intros.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   split. apply Zle_ge. apply Zle_trans with 1%Z.
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   unfold Zle in |- *. simpl in |- *. discriminate.
(* Goal: alllist Z ZPrime t *)
   apply Zlt_le_weak. apply Zgt_lt. assumption.
(* Goal: alllist Z ZPrime t *)
   apply IH. assumption.
Qed.

Lemma allprimeallzprime :
 forall l : natlist, allPrime l -> allZPrime (map _ _ Z_of_nat l).
Proof.
(* Goal: forall (l : Zlist) (_ : allZPrime l), allPrime (map Z nat Z.abs_nat l) *)
   unfold allPrime, allZPrime in |- *.
(* Goal: forall (l : Zlist) (_ : alllist Z ZPrime l), alllist nat Prime (map Z nat Z.abs_nat l) *)
   simple induction l.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   simpl in |- *. intro. assumption.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   simpl in |- *. intros h t IH H. elim H. intros. split.
(* Goal: alllist Z ZPrime t *)
   apply primezprime. assumption.
(* Goal: alllist Z ZPrime t *)
   apply IH. assumption.
Qed.

Lemma allzprimeallprime :
 forall l : Zlist, allZPrime l -> allPrime (map _ _ Zabs_nat l).
Proof.
(* Goal: forall (l : Zlist) (_ : allZPrime l), allPrime (map Z nat Z.abs_nat l) *)
   unfold allPrime, allZPrime in |- *.
(* Goal: forall (l : Zlist) (_ : alllist Z ZPrime l), alllist nat Prime (map Z nat Z.abs_nat l) *)
   simple induction l.
(* Goal: forall _ : True, True *)
(* Goal: forall (a : Z) (l : list Z) (_ : forall _ : alllist Z ZPrime l, alllist nat Prime (map Z nat Z.abs_nat l)) (_ : alllist Z ZPrime (Cons Z a l)), alllist nat Prime (map Z nat Z.abs_nat (Cons Z a l)) *)
   simpl in |- *. intro. assumption.
(* Goal: and (Prime (Z.abs_nat h)) (alllist nat Prime (map Z nat Z.abs_nat t)) *)
   simpl in |- *. intros h t IH H. elim H. intros. split.
(* Goal: alllist Z ZPrime t *)
   apply zprimeprime. assumption.
(* Goal: alllist Z ZPrime t *)
   apply IH. assumption.
Qed.
