proposition: Fact fractran_step_head_not_zero p q l y : q <> 0 -> (p,q)::l /F/ 0 ≻ y -> y = 0.
proof: Proof. intros H2 H3. apply fractran_step_cons_inv in H3. destruct H3 as [ H3 | (H3 & _) ]. + rewrite Nat.mul_0_r in H3; apply Nat.eq_mul_0 in H3; lia. + destruct H3; exists 0; ring. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)