Lecture 8 Level 1 doesn’t actually need `by_cases hk0 : k = 0`

[bluebear94]

There’s a simpler way to solve this problem:

My solution

induction' n with k hk
norm_num
have h1 : k + 1 < 2 ^ k + 2 ^ 0 := by norm_num; bound
have h2 : 2 ^ k + 2 ^ 0 ≤ 2 ^ k + 2 ^ k := by bound
have h3 : 2 ^ k + 2 ^ k = 2 ^ (k + 1) := by ring_nf
bound

Perhaps this should be noted in the description.