exists_prime_divisor@{} n : 1 < n -> exists (p : Prime), (p | n). Proof. revert n; snrapply nat_ind_strong; hnf; intros n IHn H. destruct (dec (IsPrime n)) as [x|x]. 1: exists (_; x); exact _. pose (r := (H, x)). apply not_isprime_iff_iscomposite in r. destruct r as [d [[H1 H2] H3]]. destruct (IHn d _ _) as [p r]. exists p. exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes