proposition: Lemma primeDiv : forall a : nat, 1 < a -> exists p : nat, Prime p /\ divide p a.
proof: Proof. intro a. apply (lt_wf_ind a). clear a. intros. destruct (Prime_dec n). + exists n. split; auto. exists 1. lia. + assert (~ prime (Z.of_nat n)). { intro. apply H1. apply prime_Prime. auto. } apply not_prime_divide in H2. destruct H2. destruct H2. assert (Z.to_nat x < n) by lia. assert (1 < Z.to_nat x) by lia. destruct (H _ H4 H5). destruct H6. exists x0. split; auto. destruct H3, H7. exists (Z.to_nat x1 * x2). nia. lia. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow