theorem zeqmsub1 (a b c n: nat): $ modZ(n): a -Z c = b -Z c <-> modZ(n): a = b $;
modZ(n): a +Z -uZ c = b +Z -uZ c <-> modZ(n): a = b
modZ(n): a -Z c = b -Z c <-> modZ(n): a = b