proposition: Fact fractran_step_cons_inv p q l x y : (p,q)::l /F/ x ≻ y <-> q*y = p*x \/ ~ divides q (p*x) /\ l /F/ x ≻ y.
proof: Proof. split. + inversion 1; auto. + intros [ H | (H1 & H2) ]; [ constructor 1 | constructor 2 ]; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)