proposition: Lemma Z_prime_ind : forall P : Z -> Prop, ((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; apply Z_prime_rect; auto. Qed.
imports: ZArith Lia Znumtheory Natsets MyNat Ztools Zeqm