no goals
F : Type ?u.55640
ι : Type ?u.55643
α : Type ?u.55646
β : Type ?u.55649
K : Type u_1
inst✝ : LinearOrderedField K
m n : ℚ
⊢ m < n → ↑m < ↑n
simpa only [sub_pos, cast_sub] using @cast_pos_of_pos K _ (n - m)