proposition: Lemma Z_prime_rect : forall P : Z -> Type, ((P 0) -> (P 1) -> (forall n, prime n -> P n) -> (forall a b, P a -> P b -> P (a * b)) -> forall n, 0 <= n -> P n)%Z.
proof: Proof. intros P P0 P1 Pprime Psplit. assert (Hind : forall (N : nat) n, 0 <= n -> (Z.abs_nat n < N)%nat -> P n). intro n ; induction n ; intros i ipos imax. exfalso; inversion imax. destruct (Z_le_lt_eq_dec i (Z_of_nat n)) as [|E]. lia. apply IHn; lia. rewrite E in *; clear E i ipos imax. destruct (prime_dec (Z_of_nat n)) as [Hprime | Hnprime]. apply Pprime ; assumption. destruct n. subst; apply P0. destruct n. subst; apply P1. set (z := Z_of_nat (S (S n))). assert (n_big : 1 < z) by (unfold z; lia). destruct (not_prime_divide_inf _ n_big Hnprime) as [a [[amin amax] b_eqz]]. destruct (Zdivide_inf _ _ b_eqz) as [b eqz]; clear b_eqz; rewrite eqz. assert (Bb : 1 < b < z). assert (1 < b) by (apply Zmult_lt_reg_r with a; lia). split; auto. rewrite <- (Zmult_1_r b), eqz. apply Zmult_lt_compat_l; try lia. apply Psplit; apply IHn; lia. intros n n_pos ; apply Hind with (S (Z.abs_nat n)) ; auto. Defined.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm