induction m using recBase2 generalizing n
m n : Nat
⊢ m ≤ n → log2' m ≤ log2' n
case zero
n : Nat
⊢ 0 ≤ n → log2' 0 ≤ log2' n

case one
n : Nat
⊢ 1 ≤ n → log2' 1 ≤ log2' n

case div2
n✝ : Nat
a✝ : ∀ {n : Nat}, n✝ / 2 + 1 ≤ n → log2' (n✝ / 2 + 1) ≤ log2' n
n : Nat
⊢ n✝ + 2 ≤ n → log2' (n✝ + 2) ≤ log2' n