theorem znegb0S (n: nat): $ -uZ b0 (suc n) = b1 n $;
-uZ b1 n = b0 (suc n) <-> -uZ b0 (suc n) = b1 n
-uZ b1 n = b0 (suc n)
-uZ b0 (suc n) = b1 n