proposition: Lemma FRACTRAN_HALTING_zero_num l x : Exists (fun c => fst c = 0) l -> FRACTRAN_HALTING (l,x) <-> False.
proof: Proof. intros H; split; try tauto. intros (y & _ & H3). destruct fractran_zero_num_step with (1 := H) (x := y) as (z & Hz). apply H3 with (1 := Hz). Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)