Theorem: mod_eq_sub_div_mul (Fl/Lemmas.lean)

State before:
m k : ℕ
⊢ m % k = m - m / k * k
Tactic:
apply eq_tsub_of_add_eq
State after:
case h
m k : ℕ
⊢ m % k + m / k * k = m

State before:
case h
m k : ℕ
⊢ m % k + m / k * k = m
Tactic:
exact Nat.mod_add_div' m k
State after:
no goals