m✝ n✝ k✝ m n k : ℕ
n0 : 0 < n
⊢ m < n * k + n ↔ m ≤ n * k + (n - 1)
m✝ n✝ k✝ m n k : ℕ
n0 : 0 < n
⊢ m / n ≤ k ↔ m ≤ n * k + (n - 1)
rw [← lt_succ_iff, div_lt_iff_lt_mul n0, succ_mul, mul_comm]
case zero
m✝ n k✝ m k : ℕ
n0 : 0 < zero
⊢ m < zero * k + zero ↔ m ≤ zero * k + (zero - 1)

case succ
m✝ n k✝ m k n✝ : ℕ
n0 : 0 < succ n✝
⊢ m < succ n✝ * k + succ n✝ ↔ m ≤ succ n✝ * k + (succ n✝ - 1)
m✝ n✝ k✝ m n k : ℕ
n0 : 0 < n
⊢ m < n * k + n ↔ m ≤ n * k + (n - 1)
cases n
no goals
case succ
m✝ n k✝ m k n✝ : ℕ
n0 : 0 < succ n✝
⊢ m < succ n✝ * k + succ n✝ ↔ m ≤ succ n✝ * k + (succ n✝ - 1)
exact lt_succ_iff
no goals
case zero
m✝ n k✝ m k : ℕ
n0 : 0 < zero
⊢ m < zero * k + zero ↔ m ≤ zero * k + (zero - 1)
cases n0