proposition: Theorem prime_decomp n : n <> 0 -> { l | n = lprod l /\ Forall prime l }.
proof: Proof. induction on n as IHn with measure n; intro Hn. destruct (eq_nat_dec n 1) as [ Hn' | Hn' ]. + exists nil; simpl; auto. + destruct (@prime_factor n) as (p & H1 & H2); try lia. apply divides_div in H2; revert H2. generalize (div n p); intros k Hk. assert (k <> 0) as Hk'. { intros ?; subst; destruct Hn; auto. } destruct (IHn k) as (l & H2 & H3); auto. - rewrite Hk. generalize (prime_ge_2 H1). rewrite Nat.mul_comm. destruct p as [ | [ | p ] ]; simpl; intros; lia. - exists (p::l); split; auto. simpl; rewrite <- H2, Nat.mul_comm; auto. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)