proposition: Lemma FRACTRAN_HALTING_on_zero_first_no_zero_den p q l : q <> 0 -> FRACTRAN_HALTING ((p,q)::l,0) <-> False.
proof: Proof. intros Hq; split; try tauto. intros (y & (k & H1) & H2). apply fractran_rt_head_not_zero in H1; auto. subst y; apply (H2 0); constructor 1; ring. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)