English
If 1 < b and ⌈(b−1)⁻¹⌉_+ / b < a, then ⌈a⌉_+ < b·a.
Русский
Если 1<b и ⌈(b−1)⁻¹⌉_+ / b < a, то ⌈a⌉_+ < b·a.
LaTeX
$$$$ (hb: 1 < b) \Rightarrow (hba: ⌈(b-1)^{-1}⌉_+ / b < a) \Rightarrow \lceil a \rceil_+ < b \cdot a $$$$
Lean4
theorem ceil_lt_mul (hb : 1 < b) (hba : ⌈(b - 1)⁻¹⌉₊ / b < a) : ⌈a⌉₊ < b * a :=
by
obtain hab | hba := le_total a (b - 1)⁻¹
·
calc
⌈a⌉₊ ≤ (⌈(b - 1)⁻¹⌉₊ : K) := by gcongr
_ < b * a := by rwa [← div_lt_iff₀']; positivity
· rw [← sub_pos] at hb
calc
⌈a⌉₊ < a + 1 := ceil_lt_add_one <| hba.trans' <| by positivity
_ = a + (b - 1) * (b - 1)⁻¹ := by rw [mul_inv_cancel₀]; positivity
_ ≤ a + (b - 1) * a := by gcongr
_ = b * a := by rw [sub_one_mul, add_sub_cancel]
