a b n : Int
⊢ (a - b + b) % n = (a % n - b % n + b) % n
a b n : Int
⊢ (a - b) % n = (a % n - b % n) % n
apply (emod_add_cancel_right b).mp
no goals
a b n : Int
⊢ (a - b + b) % n = (a % n - b % n + b) % n
rw [Int.sub_add_cancel, ← Int.add_emod_emod, Int.sub_add_cancel, emod_emod]