case hc
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ 0 < b ∧ b ≤ a
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ a / b = (a - b) / b + 1
rw [div_eq a, if_pos]
no goals
case hc
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ 0 < b ∧ b ≤ a
constructor <;> assumption