31. Powers of two grow fast
Prove that n < 2 ^ n for every natural number n.
omega does not know how ^ behaves, but it can treat 2 ^ k as an unknown number and reason linearly about it.
Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem and one Medium problem a week are open to every account.
1theorem solution (n : Nat) : n < 2 ^ n := by
givenLoading editor…
Type
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
n:Nat
⊢n < 2 ^ n
ReadyLn 1, Col 1Lean 4
Draft saved in this browser