proposition: Fact fractran_rt_no_zero_num l : Forall (fun c => fst c <> 0) l -> forall n x, fractran_steps l n x 0 -> x = 0.
proof: Proof. intros H; induction n as [ | n IHn ]; intros x; simpl; auto. intros (y & H1 & H2). apply IHn in H2. revert H1 H2; apply fractran_step_no_zero_num; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)