proposition: Lemma fractran_empty_decision (n: nat) : ([] /F/ n ↓).
proof: Proof. exists n. split; [now exists 0|]. intros z H. now inversion H. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)