prime_factorization@{} n : 0 < n -> exists (l : list Prime), n = fold_right (fun (p : Prime) n => nat_mul p n) 1 l. Proof. revert n; snrapply nat_ind_strong; hnf; intros n IHn H. destruct H as [|n IH]. 1: exists nil; reflexivity. destruct (exists_prime_divisor n.+1 _) as [p d]. pose proof (l := lt_divides d.1 n.+1 _ _ _). destruct d as [k H]. destruct (IHn k l) as [f r]. { destruct H, k. 1: contradiction (lt_irrefl 0). exact _. } exists (p :: f)%list. simpl; destruct r. symmetry. lhs nrapply nat_mul_comm. exact H. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.Classes