theorem eqzeqm (a b n: nat): $ a = b -> modZ(n): a = b $;
modZ(n): a = a
a = b -> (modZ(n): a = a <-> modZ(n): a = b)
a = b -> modZ(n): a = b