n : Nat
⊢ (if n ≥ 2 then log2 (n / 2) + 1 else 0) ≤ n
n : Nat
⊢ log2 n ≤ n
unfold Nat.log2
case inl
n : Nat
h✝ : n ≥ 2
⊢ log2 (n / 2) + 1 ≤ n

case inr
n : Nat
h✝ : ¬n ≥ 2
⊢ 0 ≤ n
n : Nat
⊢ (if n ≥ 2 then log2 (n / 2) + 1 else 0) ≤ n
split
no goals
case inl
n : Nat
h✝ : n ≥ 2
⊢ log2 (n / 2) + 1 ≤ n
next h =>
have := log2_le_self (n / 2)
exact Nat.lt_of_le_of_lt this (Nat.div_lt_self (Nat.le_of_lt h) (by decide))
n : Nat
h : n ≥ 2
this : log2 (n / 2) ≤ n / 2
⊢ log2 (n / 2) + 1 ≤ n
n : Nat
h : n ≥ 2
⊢ log2 (n / 2) + 1 ≤ n
have := log2_le_self (n / 2)
no goals
n : Nat
h : n ≥ 2
this : log2 (n / 2) ≤ n / 2
⊢ log2 (n / 2) + 1 ≤ n
exact Nat.lt_of_le_of_lt this (Nat.div_lt_self (Nat.le_of_lt h) (by decide))
no goals
n : Nat
h : n ≥ 2
this : log2 (n / 2) ≤ n / 2
⊢ 1 < 2
decide
no goals
case inr
n : Nat
h✝ : ¬n ≥ 2
⊢ 0 ≤ n
apply Nat.zero_le
no goals
n : Nat
a✝ : ∀ (y : Nat), (invImage (fun a => sizeOf a) instWellFoundedRelation).1 y n → log2 y ≤ y
h✝ : n ≥ 2
⊢ (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (n / 2) n
exact Nat.log2_terminates _ ‹_›