lean_workbook_plus_15682
ProvedProve for using induction.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15682 (k : ℕ) (h₁ : 3 ≤ k) : 2 ^ (k + 1) > 4 * k + 1 := by sorry
Source
Prove for using induction.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_15682 (k : ℕ) (h₁ : 3 ≤ k) : 2 ^ (k + 1) > 4 * k + 1 := by sorry