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

State before:
n k m : Nat
h : n < k * (m + 1)
⊢ n / k ≤ m
Tactic:
have hk : 0 < k := match k with
  | 0 => by rw [Nat.zero_mul] at h; absurd h; exact Nat.not_lt_zero _
  | _+1 => Nat.zero_lt_succ _
State after:
n k m : Nat
h : n < k * (m + 1)
hk : 0 < k
⊢ n / k ≤ m

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

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

State before:
n k m : Nat
h : n < 0 * (m + 1)
⊢ 0 < 0
Tactic:
rw [Nat.zero_mul] at h
State after:
n k m : Nat
h : n < 0
⊢ 0 < 0

State before:
n k m : Nat
h : n < 0
⊢ 0 < 0
Tactic:
absurd h
State after:
n k m : Nat
h : n < 0
⊢ ¬n < 0

State before:
n k m : Nat
h : n < 0
⊢ ¬n < 0
Tactic:
exact Nat.not_lt_zero _
State after:
no goals