proposition: Theorem prime_decomp_uniq l m : Forall prime l -> Forall prime m -> lprod l = lprod m -> l ~p m.
proof: Proof. intros H; revert H m. induction 1 as [ | x l Hx Hl IHl ]. + induction 1 as [ | y m Hy Hm IHm ]; simpl; auto. intros C; exfalso. assert (2*1 <= y*lprod m) as D. { apply Nat.mul_le_mono; auto. } simpl in D; lia. + simpl; intros m Hm H1. assert (In x m) as H2. { apply prime_in_decomp with (1 := Hx); auto. exists (lprod l); rewrite Nat.mul_comm; auto. } apply in_split in H2. destruct H2 as (m1 & m2 & H2); subst. apply Permutation_cons_app, IHl. * rewrite Forall_app in Hm. destruct Hm as [ ? Hm ]. inversion Hm. apply Forall_app; auto. * rewrite lprod_app. rewrite lprod_app in H1; simpl in H1. rewrite Nat.mul_assoc, (Nat.mul_comm _ x), <- Nat.mul_assoc in H1. apply Nat.mul_cancel_l in H1; auto. apply prime_ge_2 in Hx; lia. Qed.
imports: List Arith Lia Bool Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat gcd sums)