proposition: Lemma prime_divides_lt' {c d} (Hc : c <> 0) (Hd : d <> 0): ~ (divides d c) -> exists p, (forall x y, (S x) * c = (S y) * d -> count_pow p y < count_pow p x).
proof: Proof. pose proof (@prime_decomp c Hc) as [lc [Hclc Hlc]]. pose proof (@prime_decomp d Hd) as [ld [Hdld Hld]]. subst. intros H. apply prime_divides_lt in H as [p [? Hp]]; [|assumption ..]. exists p. intros x y. unfold count_pow. destruct (@prime_decomp (S x) _) as [lx [Hxlx Hlx]]. destruct (@prime_decomp (S y) _) as [ly [Hyly Hly]]. rewrite Hxlx, Hyly, <- !lprod_app. intros E. apply prime_decomp_uniq in E; [|now rewrite Forall_app ..]. assert (iffLR : forall P Q, (P <-> Q) -> P -> Q) by tauto. assert (H' := iffLR _ _ (Permutation_count_occ Nat.eq_dec _ _) E p). rewrite !count_occ_app in H'. lia. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)