proposition: Lemma fractran_nstop_cons a b l s : (forall t, ~ l /F/ t ↓) -> ~ (a,b) :: l /F/ s ↓.
proof: Proof. intros H [u [[n Hsu] Hu]]. destruct (divides_dec (a*u) b) as [[t Ht]|?]. - apply (Hu t), in_fractran_0. lia. - apply (H u). exists u. split; [now exists 0|]. intros t Hut. now apply (Hu t), in_fractran_1. Qed.
imports: Coq(List Arith Lia Permutation Wf_nat) Undecidability.Shared.Libs.DLW(gcd prime) Undecidability.FRACTRAN(FRACTRAN fractran_utils)