Theorem: Nat.div_eq_sub_div (Runtime/Utilities/Std.lean)

State before:
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ a / b = (a - b) / b + 1
Tactic:
rw [div_eq a, if_pos]
State after:
case hc
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ 0 < b ∧ b ≤ a

State before:
case hc
b a : Nat
h₁ : 0 < b
h₂ : b ≤ a
⊢ 0 < b ∧ b ≤ a
Tactic:
constructor <;> assumption
State after:
no goals