exact zero_le _
case hz
n : ℕ
⊢ size 0 ≤ log 2 0 + 1

case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n ≤ log 2 n + 1 → size (bit b n) ≤ log 2 (bit b n) + 1
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ), (n = 0 → b = true) → size n ≤ log 2 n + 1 → size (bit b n) ≤ log 2 (bit b n) + 1