Theorem: ℤα.div_add_mod (Mordell4/Rt7Ring.lean)

State before:
a b c : ℤα
⊢ b * (a / b) + a % b = a
Tactic:
change b * div a b + mod a b = a
State after:
a b c : ℤα
⊢ b * div a b + mod a b = a

State before:
a b c : ℤα
⊢ b * div a b + mod a b = a
Tactic:
simp [mod]
State after:
no goals