proposition: Lemma fractran_nstop_zero_num_1 d l s : ~ (0,d) :: l /F/ s ↓.
proof: Proof. destruct d as [|d]; simpl; intros [y [_ Hs]]; apply (Hs 0); now constructor. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)