proposition: Lemma FRACTRAN_HALTING_nil_x x : FRACTRAN_HALTING (nil,x) <-> True.
proof: Proof. split; try tauto; intros _. exists x; split. + exists 0; simpl; auto. + inversion 1. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)