a b c : Int
h : a % b = c
hx : a % b % b = c % b
⊢ b ∣ a - c
a b c : Int
h : a % b = c
⊢ b ∣ a - c
have hx : (a % b) % b = c % b := by
  rw [h]
a b c : Int
h : a % b = c
hx : (a - c) % b = 0
⊢ b ∣ a - c
a b c : Int
h : a % b = c
hx : a % b % b = c % b
⊢ b ∣ a - c
rw [Int.emod_emod, ← emod_sub_cancel_right c, Int.sub_self, zero_emod] at hx
no goals
a b c : Int
h : a % b = c
hx : (a - c) % b = 0
⊢ b ∣ a - c
exact dvd_of_emod_eq_zero hx
no goals
a b c : Int
h : a % b = c
⊢ a % b % b = c % b
rw [h]