proposition: Lemma fractran_step_bound l : fractran_regular l -> { k | forall x y, l /F/ x ≻ y -> y <= k*x }.
proof: Proof. unfold fractran_regular. induction l as [ | (p,q) l IHl ]. + intros _; exists 1; auto. intros ? ? H; exfalso; revert H; apply fractran_step_nil_inv. + intros H; rewrite Forall_cons_inv in H; simpl in H. destruct H as (Hq & H). destruct (IHl H) as (k & H2). exists (p+k). intros x y Hxy. apply fractran_step_cons_inv in Hxy. destruct Hxy as [ Hxy | (_ & Hxy) ]. * rewrite Nat.mul_add_distr_r, <- Hxy. destruct q; simpl; try lia. * apply Nat.le_trans with (1 := H2 _ _ Hxy). apply Nat.mul_le_mono; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)