proposition: Lemma prime_divides_lt {lc ld} : ~ (divides (lprod ld) (lprod lc)) -> Forall prime lc -> Forall prime ld -> exists (p : nat), prime p /\ count_occ Nat.eq_dec lc p < count_occ Nat.eq_dec ld p.
proof: Proof. revert lc. induction ld as [|a ld IHld]. - intros lc H. exfalso. apply H. exists (lprod lc). cbn. lia. - intros lc H Hlc Hld'. pose proof (Ha := Forall_inv Hld'). pose proof (Hld := Forall_inv_tail Hld'). destruct (in_dec Nat.eq_dec a lc) as [Halc|Halc]. + apply in_split in Halc as [l1c [l2c ?]]. subst lc. assert (H' : not (divides (lprod (ld)) (lprod (l1c ++ l2c)))). { intros [p Hp]. rewrite !lprod_app in *. apply H. exists p. cbn. nia. } assert (H'lc : Forall prime (l1c ++ l2c)). { revert Hlc. rewrite !Forall_app. now intros [? ? %Forall_inv_tail]. } specialize (IHld _ H' H'lc Hld). destruct IHld as [p [? Hp]]. exists p. split; [assumption|]. revert Hp. rewrite !count_occ_app. cbn. destruct (Nat.eq_dec); lia. + exists a. split; [assumption|]. apply (count_occ_not_In Nat.eq_dec) in Halc. rewrite count_occ_cons_eq, Halc; lia. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)