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