case hnc
a b : Nat
h₀ : a < b
⊢ ¬(0 < b ∧ b ≤ a)
a b : Nat
h₀ : a < b
⊢ a / b = 0
rw [div_eq a, if_neg]
case hnc
a b : Nat
h₀ : a < b
h₁ : 0 < b ∧ b ≤ a
⊢ False
case hnc
a b : Nat
h₀ : a < b
⊢ ¬(0 < b ∧ b ≤ a)
intro h₁
no goals
case hnc
a b : Nat
h₀ : a < b
h₁ : 0 < b ∧ b ≤ a
⊢ False
apply Nat.not_le_of_gt h₀ h₁.right