no goals
n k : Nat
⊢ n / k ≤ n
induction n using Nat.strongInductionOn 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)
case ind
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 ≤ n
case ind
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
⊢ n / k ≤ n
rw [div_eq]
no goals
case ind
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 ≤ n
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)
no goals
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
simp [h]
case ind.isTrue
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
⊢ (n - k) / k + 1 ≤ n
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
suffices (n - k) / k + 1 ≤ n by simp [h, this]
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
case ind.isTrue
k n : Nat
ih : ∀ (m : Nat), m < n → m / k ≤ m
h : 0 < k ∧ k ≤ n
⊢ (n - k) / k + 1 ≤ n
have ⟨hK, hKN⟩ := h
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
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
have hSub : n - k < n := sub_lt (Nat.lt_of_lt_of_le hK hKN) hK
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
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
have : (n - k) / k ≤ n - k := ih (n - k) hSub
no goals
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
exact succ_le_of_lt (Nat.lt_of_le_of_lt this hSub)
no goals
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
simp [h, this]