proposition: Lemma fractran_rt_no_zero_den_0_0 l : l <> nil -> fractran_regular l -> fractran_step l 0 0.
proof: Proof. destruct l as [ | (p,q) l ]; intros H1 H. + destruct H1; auto. + clear H1; apply Forall_cons_inv, proj1 in H. constructor 1; ring. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)