theorem zdvdeq1 (_m1 _m2 n: nat): $ _m1 = _m2 -> (_m1 |Z n <-> _m2 |Z n) $;
_m1 = _m2 -> _m1 = _m2
_m1 = _m2 -> (_m1 |Z n <-> _m2 |Z n)