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

State before:
m n k : Nat
h : m ≤ n
⊢ m / k ≤ n / k
Tactic:
match k with
| 0 => rw [Nat.div_zero]; exact Nat.zero_le _
| k+1 =>
  apply Nat.div_le_of_lt_mul_succ
  apply Nat.lt_of_le_of_lt h
  conv => lhs; rw [←Nat.div_add_mod n (k+1)]
  rw [Nat.mul_succ, Nat.add_lt_add_iff_left]
  exact Nat.mod_lt _ (Nat.zero_lt_succ _)
State after:
no goals

State before:
m n k : Nat
h : m ≤ n
⊢ m / 0 ≤ n / 0
Tactic:
rw [Nat.div_zero]
State after:
m n k : Nat
h : m ≤ n
⊢ 0 ≤ n / 0

State before:
m n k : Nat
h : m ≤ n
⊢ 0 ≤ n / 0
Tactic:
exact Nat.zero_le _
State after:
no goals

State before:
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ m / (k + 1) ≤ n / (k + 1)
Tactic:
apply Nat.div_le_of_lt_mul_succ
State after:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ m < (k + 1) * (n / (k + 1) + 1)

State before:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ m < (k + 1) * (n / (k + 1) + 1)
Tactic:
apply Nat.lt_of_le_of_lt h
State after:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ n < (k + 1) * (n / (k + 1) + 1)

State before:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ n < (k + 1) * (n / (k + 1) + 1)
Tactic:
conv => lhs; rw [←Nat.div_add_mod n (k+1)]
State after:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ (k + 1) * (n / (k + 1)) + n % (k + 1) < (k + 1) * (n / (k + 1) + 1)

State before:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ (k + 1) * (n / (k + 1)) + n % (k + 1) < (k + 1) * (n / (k + 1) + 1)
Tactic:
rw [Nat.mul_succ, Nat.add_lt_add_iff_left]
State after:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ n % (k + 1) < k + 1

State before:
case h
m n k✝ : Nat
h : m ≤ n
k : Nat
⊢ n % (k + 1) < k + 1
Tactic:
exact Nat.mod_lt _ (Nat.zero_lt_succ _)
State after:
no goals