z x y : Nat
⊢ z * x % (z * y) = z * (x % y)
z x y : Nat
⊢ x * z % (y * z) = x % y * z
rw [Nat.mul_comm x z, Nat.mul_comm y z, Nat.mul_comm (x % y) z]
no goals
z x y : Nat
⊢ z * x % (z * y) = z * (x % y)
apply mul_mod_mul_left