proposition: Fact fractran_rt_no_zero_den l n y : fractran_regular l -> fractran_steps l n 0 y -> y = 0.
proof: Proof. intros H; induction n as [ | n IHn ]. + simpl; auto. + intros (x & H1 & H2). apply fractran_step_no_zero_den with (1 := H) in H1; subst; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)