proposition: Fact fractran_step_no_zero_num l : Forall (fun c => fst c <> 0) l -> forall x y, l /F/ x ≻ y -> y = 0 -> x = 0.
proof: Proof. intros H1 x y H2; revert H2 H1. induction 1 as [ p q l x y H1 | p q l x y H1 H2 IH2 ]; intros H3; rewrite Forall_cons_inv in H3; simpl in H3; destruct H3 as (H3 & H4); auto. intros; subst y; rewrite Nat.mul_0_r in H1; symmetry in H1; apply Nat.eq_mul_0 in H1; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)