a b : Int
this : (a + b * 1) % b = a % b
⊢ (a + b) % b = a % b
a b : Int
⊢ (a + b) % b = a % b
have := add_mul_emod_self_left a b 1
no goals
a b : Int
this : (a + b * 1) % b = a % b
⊢ (a + b) % b = a % b
rwa [Int.mul_one] at this