proposition: Fact fractran_step_dec l x : { y | l /F/ x ≻ y } + { fractran_stop l x }.
proof: Proof. induction l as [ | (a,b) l IH ]. + right; rewrite fractan_stop_nil_inv; auto. + destruct (divides_dec (a*x) b) as [ (y & Hy) | ]. * left; exists y; constructor 1; rewrite Hy; ring. * destruct IH as [ (y & ?) | ]. - left; exists y; now constructor 2. - right; apply fractan_stop_cons_inv; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)