no goals
m n : Nat
x✝ : m ≤ 0 * n
⊢ m / 0 ≤ n
simp [Nat.div_zero, n.zero_le]
m n k : Nat
h : m ≤ succ k * n
⊢ succ k * (m / succ k) ≤ succ k * n
m n k : Nat
h : m ≤ succ k * n
⊢ m / succ k ≤ n
suffices succ k * (m / succ k) ≤ succ k * n from
  Nat.le_of_mul_le_mul_left this (zero_lt_succ _)
m n k : Nat
h : m ≤ succ k * n
h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k)
⊢ succ k * (m / succ k) ≤ succ k * n
m n k : Nat
h : m ≤ succ k * n
⊢ succ k * (m / succ k) ≤ succ k * n
have h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k) := Nat.le_add_left _ _
m n k : Nat
h : m ≤ succ k * n
h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k)
h2 : m % succ k + succ k * (m / succ k) = m
⊢ succ k * (m / succ k) ≤ succ k * n
m n k : Nat
h : m ≤ succ k * n
h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k)
⊢ succ k * (m / succ k) ≤ succ k * n
have h2 : m % succ k + succ k * (m / succ k) = m := by rw [mod_add_div]
m n k : Nat
h : m ≤ succ k * n
h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k)
h2 : m % succ k + succ k * (m / succ k) = m
h3 : m ≤ succ k * n
⊢ succ k * (m / succ k) ≤ succ k * n
m n k : Nat
h : m ≤ succ k * n
h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k)
h2 : m % succ k + succ k * (m / succ k) = m
⊢ succ k * (m / succ k) ≤ succ k * n
have h3 : m ≤ succ k * n := h
m n k : Nat
h : m ≤ succ k * n
h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k)
h2 : m % succ k + succ k * (m / succ k) = m
h3 : m % succ k + succ k * (m / succ k) ≤ succ k * n
⊢ succ k * (m / succ k) ≤ succ k * n
m n k : Nat
h : m ≤ succ k * n
h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k)
h2 : m % succ k + succ k * (m / succ k) = m
h3 : m ≤ succ k * n
⊢ succ k * (m / succ k) ≤ succ k * n
rw [← h2] at h3
no goals
m n k : Nat
h : m ≤ succ k * n
h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k)
h2 : m % succ k + succ k * (m / succ k) = m
h3 : m % succ k + succ k * (m / succ k) ≤ succ k * n
⊢ succ k * (m / succ k) ≤ succ k * n
exact Nat.le_trans h1 h3
no goals
m n k : Nat
h : m ≤ succ k * n
h1 : succ k * (m / succ k) ≤ m % succ k + succ k * (m / succ k)
⊢ m % succ k + succ k * (m / succ k) = m
rw [mod_add_div]