n k : Nat
hLtN : 0 < n
hLtK : 1 < k
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 < n
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
⊢ n / k < n
rw [div_eq]
no goals
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 < n
cases (inferInstance : Decidable (0 < k ∧ k ≤ n)) with
| isFalse h => simp [hLtN, h]
| isTrue h =>
  suffices (n - k) / k + 1 < n by simp [h, this]
  have ⟨_, hKN⟩ := h
  have : (n - k) / k ≤ n - k := div_le_self (n - k) k
  have := Nat.add_le_of_le_sub hKN this
  exact Nat.lt_of_lt_of_le (Nat.add_lt_add_left hLtK _) this
no goals
case isFalse
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : ¬(0 < k ∧ k ≤ n)
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 < n
simp [hLtN, h]
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
⊢ (n - k) / k + 1 < n
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
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 isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
⊢ (n - k) / k + 1 < n
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
⊢ (n - k) / k + 1 < n
have ⟨_, hKN⟩ := h
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
this : (n - k) / k ≤ n - k
⊢ (n - k) / k + 1 < n
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
⊢ (n - k) / k + 1 < n
have : (n - k) / k ≤ n - k := div_le_self (n - k) k
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
this✝ : (n - k) / k ≤ n - k
this : (n - k) / k + k ≤ n
⊢ (n - k) / k + 1 < n
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
this : (n - k) / k ≤ n - k
⊢ (n - k) / k + 1 < n
have := Nat.add_le_of_le_sub hKN this
no goals
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
this✝ : (n - k) / k ≤ n - k
this : (n - k) / k + k ≤ n
⊢ (n - k) / k + 1 < n
exact Nat.lt_of_lt_of_le (Nat.add_lt_add_left hLtK _) this
no goals
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
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]