proposition: Lemma fractran_singleton_decision c d n : ([(c,d)] /F/ n ↓) + (not ([(c,d)] /F/ n ↓)).
proof: Proof. destruct (divides_dec c d) as [[k Hk] | Hndiv]. { right. intros [y [[m Hm] Hstop]]. apply (Hstop (k*y)). constructor. nia. } destruct c as [|c]. { right. now intros H%fractran_nstop_zero_num_1. } destruct d as [|d]. { left. now apply fractran_stop_zero_den_1. } destruct n as [|n]. { right. intros [y [[n Hn] Hy]]. apply fractran_rt_no_zero_den in Hn. - apply (Hy 0). apply in_fractran_0. lia. - now repeat constructor. } left. now apply fractran_stop_ndiv_singleton. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)