m n k i : Int
H : (m + i) % n = (k + i) % n
this : (m + i + -i) % n = (k + i + -i) % n
⊢ m % n = k % n
m n k i : Int
H : (m + i) % n = (k + i) % n
⊢ m % n = k % n
have := add_emod_eq_add_emod_right (-i) H
no goals
m n k i : Int
H : (m + i) % n = (k + i) % n
this : (m + i + -i) % n = (k + i + -i) % n
⊢ m % n = k % n
rwa [Int.add_neg_cancel_right, Int.add_neg_cancel_right] at this