theorem zsubpos (m n: nat): $ n <= m -> b0 m -Z b0 n = b0 (m - n) $;
b0 m -Z b0 n = m -ZN n
n <= m -> m -ZN n = b0 (m - n)
n <= m -> b0 m -Z b0 n = b0 (m - n)