-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_le_self (n k : Nat) : n / k ≤ n

Proof state:
case ind.isTrue
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 ≤ n

Tactic:
suffices (n - k) / k + 1 ≤ n by simp [h, this]

Result:
case ind.isTrue
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
⊢ (n - k) / k + 1 ≤ n

Proof state:
case ind
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 ≤ n

Tactic:
cases (inferInstance : Decidable (0 < k ∧ k ≤ n)) with
| isFalse h => simp [h]
| isTrue h =>
  suffices (n - k) / k + 1 ≤ n by simp [h, this]
  have ⟨hK, hKN⟩ := h
  have hSub : n - k < n := sub_lt (Nat.lt_of_lt_of_le hK hKN) hK
  have : (n - k) / k ≤ n - k := ih (n - k) hSub
  exact succ_le_of_lt (Nat.lt_of_le_of_lt this hSub)

Result:
no goals

Proof state:
case ind.isTrue
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
⊢ (n - k) / k + 1 ≤ n

Tactic:
have ⟨hK, hKN⟩ := h

Result:
case ind.isTrue
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
hK : 0 < k
hKN : k ≤ n
⊢ (n - k) / k + 1 ≤ n

Proof state:
case ind.isFalse
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : ¬(0 < k ∧ k ≤ n)
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 ≤ n

Tactic:
simp [h]

Result:
no goals

Proof state:
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
this : (n - k) / k + 1 ≤ n
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 ≤ n

Tactic:
simp [h, this]

Result:
no goals

Proof state:
n k : Nat
⊢ n / k ≤ n

Tactic:
induction n using Nat.strongRecOn with
| ind n ih =>
  rw [div_eq]
  cases (inferInstance : Decidable (0 < k ∧ k ≤ n)) with
  | isFalse h => simp [h]
  | isTrue h =>
    suffices (n - k) / k + 1 ≤ n by simp [h, this]
    have ⟨hK, hKN⟩ := h
    have hSub : n - k < n := sub_lt (Nat.lt_of_lt_of_le hK hKN) hK
    have : (n - k) / k ≤ n - k := ih (n - k) hSub
    exact succ_le_of_lt (Nat.lt_of_le_of_lt this hSub)

Result:
no goals

Proof state:
case ind.isTrue
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
hK : 0 < k
hKN : k ≤ n
hSub : n - k < n
this : (n - k) / k ≤ n - k
⊢ (n - k) / k + 1 ≤ n

Tactic:
exact succ_le_of_lt (Nat.lt_of_le_of_lt this hSub)

Result:
no goals

Proof state:
case ind
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
⊢ n / k ≤ n

Tactic:
rw [div_eq]

Result:
case ind
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 ≤ n

Proof state:
case ind.isTrue
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
hK : 0 < k
hKN : k ≤ n
hSub : n - k < n
⊢ (n - k) / k + 1 ≤ n

Tactic:
have : (n - k) / k ≤ n - k := ih (n - k) hSub

Result:
case ind.isTrue
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
hK : 0 < k
hKN : k ≤ n
hSub : n - k < n
this : (n - k) / k ≤ n - k
⊢ (n - k) / k + 1 ≤ n

Proof state:
case ind.isTrue
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
hK : 0 < k
hKN : k ≤ n
⊢ (n - k) / k + 1 ≤ n

Tactic:
have hSub : n - k < n := sub_lt (Nat.lt_of_lt_of_le hK hKN) hK

Result:
case ind.isTrue
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
hK : 0 < k
hKN : k ≤ n
hSub : n - k < n
⊢ (n - k) / k + 1 ≤ n