lean_workbook_plus_76254
Provedprove that for all
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_76254 (k : ℕ) (h : 1 ≤ k) : k + 1 ≤ 2 ^ k := by sorry
Source
prove that for all
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_76254 (k : ℕ) (h : 1 ≤ k) : k + 1 ≤ 2 ^ k := by sorry