m n k : Nat
this : (m % n + k) % n = (m % n + k + n * (m / n)) % n
⊢ (m % n + k) % n = (m + k) % n
m n k : Nat
⊢ (m % n + k) % n = (m + k) % n
have := (add_mul_mod_self_left (m % n + k) n (m / n)).symm
no goals
m n k : Nat
this : (m % n + k) % n = (m % n + k + n * (m / n)) % n
⊢ (m % n + k) % n = (m + k) % n
rwa [Nat.add_right_comm, mod_add_div] at this