proposition: Corollary FRACTRAN_HALTING_0_num l x : Exists (fun c => fst c = 0) l -> FRACTRAN_HALTING (l,x) <-> False.
proof: Proof. intros H1; split; try tauto; intros (y & H2 & H3). destruct (fractran_zero_num y H1) as (z & ?). apply (H3 z); auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)