English
For any rational q, its numerator is strictly less than (floor(q) + 1) times the denominator; i.e. q.num < (⌊q⌋ + 1) q.den.
Русский
Для любой рациональной q числитель меньше чем (⌊q⌋ + 1) умножить на знаменатель.
LaTeX
$$$$ q.num < (\\lfloor q \\rfloor + 1) \\cdot q.den, \\quad q \\in \\mathbb{Q}. $$$$
Lean4
theorem num_lt_succ_floor_mul_den (q : ℚ) : q.num < (⌊q⌋ + 1) * q.den :=
by
suffices (q.num : ℚ) < (⌊q⌋ + 1) * q.den from mod_cast this
suffices (q.num : ℚ) < (q - fract q + 1) * q.den
by
have : (⌊q⌋ : ℚ) = q - fract q := eq_sub_of_add_eq <| floor_add_fract q
rwa [this]
suffices (q.num : ℚ) < q.num + (1 - fract q) * q.den
by
have : (q - fract q + 1) * q.den = q.num + (1 - fract q) * q.den := by
calc
(q - fract q + 1) * q.den = (q + (1 - fract q)) * q.den := by ring
_ = q * q.den + (1 - fract q) * q.den := by rw [add_mul]
_ = q.num + (1 - fract q) * q.den := by simp
rwa [this]
suffices 0 < (1 - fract q) * q.den by
rw [← sub_lt_iff_lt_add']
simpa
have : 0 < 1 - fract q := by
have : fract q < 1 := fract_lt_one q
have : 0 + fract q < 1 := by simp [this]
rwa [lt_sub_iff_add_lt]
exact mul_pos this (by exact mod_cast q.pos)
