Theorem: BrownCs22.Nat.quotient_remainder (BrownCs22/Library/Defs.lean)

State before:
a b c : ℕ
h : a % b = c
⊢ ∃ q, a = q * b + c
Tactic:
use a/b
State after:
case h
a b c : ℕ
h : a % b = c
⊢ a = a / b * b + c

State before:
case h
a b c : ℕ
h : a % b = c
⊢ a = a / b * b + c
Tactic:
rw [← h, mul_comm, Nat.div_add_mod]
State after:
no goals