no goals
ι : Type ?u.345892
ι' : Type ?u.345895
α : Type ?u.345898
β : Type ?u.345901
γ : Type ?u.345904
k : ℕ
hk : 0 < k
a b : ℕ
x✝ : b ≥ 1
⊢ a / k ≤ b ↔ a ≤ (fun b => b * k + (k - 1)) b
simp only [← Nat.lt_succ_iff, Nat.div_lt_iff_lt_mul hk, Nat.succ_eq_add_one,
add_assoc, tsub_add_cancel_of_le (Nat.one_le_iff_ne_zero.2 hk.ne'), add_mul, one_mul]
no goals
ι : Type ?u.345892
ι' : Type ?u.345895
α : Type ?u.345898
β : Type ?u.345901
γ : Type ?u.345904
k : ℕ
hk : 0 < k
b : ℕ
x✝ : b ≥ 1
⊢ b = b * k / k
rw [Nat.mul_div_cancel b hk]