prove "a ≡ b + k*m → a mod m ≡ b mod m" and use it to simplify the proof of mod-dist-+
prove mod-dist-*