Theorem: Nat.div_le_iff_lt_mul_succ (Extra/Nat/Lemmas.lean)

State before:
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ n < k * (m + 1)
Tactic:
rw [←Nat.div_add_mod n k, Nat.mul_succ]
State after:
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ k * (n / k) + n % k < k * m + k

State before:
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ k * (n / k) + n % k < k * m + k
Tactic:
apply Nat.lt_of_succ_le
State after:
case h
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ (k * (n / k) + n % k).succ ≤ k * m + k

State before:
case h
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ (k * (n / k) + n % k).succ ≤ k * m + k
Tactic:
apply Nat.add_le_add _ (Nat.mod_lt _ k0)
State after:
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ k * (n / k) ≤ k * m

State before:
k n m : Nat
k0 : 0 < k
h : n / k ≤ m
⊢ k * (n / k) ≤ k * m
Tactic:
exact Nat.mul_le_mul_left _ h
State after:
no goals

State before:
k n m : Nat
k0 : 0 < k
h : n < k * (m + 1)
⊢ n / k ≤ m
Tactic:
rw [Nat.mul_comm, ←Nat.div_lt_iff_lt_mul k0] at h
State after:
k n m : Nat
k0 : 0 < k
h : n / k < m + 1
⊢ n / k ≤ m

State before:
k n m : Nat
k0 : 0 < k
h : n / k < m + 1
⊢ n / k ≤ m
Tactic:
exact Nat.le_of_lt_succ h
State after:
no goals