theorem znsubeq1 (_m1 _m2 n: nat): $ _m1 = _m2 -> _m1 -ZN n = _m2 -ZN n $;
_m1 = _m2 -> _m1 = _m2
_m1 = _m2 -> _m1 -ZN n = _m2 -ZN n