lean_workbook_plus_10412
ProvedObserve that (an easy practice on induction).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10412 (k : ℕ) (h : 1 ≤ k) : 2 ^ (k - 1) ≥ k := by sorry
Source
Observe that (an easy practice on induction).
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_10412 (k : ℕ) (h : 1 ≤ k) : 2 ^ (k - 1) ≥ k := by sorry