no goals
n k : Nat
h : n ≠ 0
⊢ 0 ≤ log2 n ↔ 2 ^ 0 ≤ n
simp [show 1 ≤ n from Nat.pos_of_ne_zero h]
n k✝ : Nat
h : n ≠ 0
k : Nat
⊢ (k + 1 ≤ if n ≥ 2 then log2 (n / 2) + 1 else 0) ↔ 2 ^ (k + 1) ≤ n
n k✝ : Nat
h : n ≠ 0
k : Nat
⊢ k + 1 ≤ log2 n ↔ 2 ^ (k + 1) ≤ n
rw [log2]
case inl
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
⊢ k + 1 ≤ log2 (n / 2) + 1 ↔ 2 ^ (k + 1) ≤ n

case inr
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ k + 1 ≤ 0 ↔ 2 ^ (k + 1) ≤ n
n k✝ : Nat
h : n ≠ 0
k : Nat
⊢ (k + 1 ≤ if n ≥ 2 then log2 (n / 2) + 1 else 0) ↔ 2 ^ (k + 1) ≤ n
split
case inl
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
n0 : 0 < n / 2
⊢ k + 1 ≤ log2 (n / 2) + 1 ↔ 2 ^ (k + 1) ≤ n
case inl
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
⊢ k + 1 ≤ log2 (n / 2) + 1 ↔ 2 ^ (k + 1) ≤ n
have n0 : 0 < n / 2 := (Nat.le_div_iff_mul_le (by decide)).2 ‹_›
no goals
case inl
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
n0 : 0 < n / 2
⊢ k + 1 ≤ log2 (n / 2) + 1 ↔ 2 ^ (k + 1) ≤ n
simp [Nat.add_le_add_iff_le_right, le_log2 (Nat.ne_of_gt n0), le_div_iff_mul_le, Nat.pow_succ]
no goals
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : n ≥ 2
⊢ 0 < 2
decide
case inr
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ ¬2 ^ (k + 1) ≤ n
case inr
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ k + 1 ≤ 0 ↔ 2 ^ (k + 1) ≤ n
simp only [le_zero_eq, succ_ne_zero, false_iff]
case inr
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ 2 ≤ 2 ^ (k + 1)
case inr
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ ¬2 ^ (k + 1) ≤ n
refine mt (Nat.le_trans ?_) ‹_›
no goals
case inr
n k✝ : Nat
h : n ≠ 0
k : Nat
h✝ : ¬n ≥ 2
⊢ 2 ≤ 2 ^ (k + 1)
exact Nat.pow_le_pow_of_le_right (Nat.succ_pos 1) (Nat.le_add_left 1 k)