proposition: Fact fractran_rt_head_not_zero p q l n y : q <> 0 -> fractran_steps ((p,q)::l) n 0 y -> y = 0.
proof: Proof. intros H2. induction n as [ | n IHn ]. + simpl; auto. + intros (a & H3 & H4). apply fractran_step_head_not_zero in H3; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)