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