proposition: Fact fractran_step_no_zero_den l x y : fractran_regular l -> l /F/ x ≻ y -> x = 0 -> y = 0.
proof: Proof. unfold fractran_regular. intros H1 H2; revert H2 H1. induction 1 as [ p q l x y H | p q l x y H1 H2 IH2 ]; rewrite Forall_cons_inv; simpl; intros (H3 & H4) ?; subst. + rewrite Nat.mul_0_r in H; apply Nat.eq_mul_0 in H; lia. + destruct H1; exists 0; ring. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)