One-liner proof for exp_larger

Changes

1 changed files (+1/-5)

• Sum.lean
  • @@ -29,11 +29,7 @@ lemma telescope_sum (n : ℕ) (h : 2 ≤ n) : ∑ a ∈ Ico 2 n, ∑ b ∈ Ico 2
    -- Exponentials grow quickly lemma exp_larger (n : ℕ) (h : 2 ≤ n) : (n - 2) * 2 ≤ 2 ^ (n - 1) := by - by_cases h : 2 < n - · induction h - · decide - · grind [mul_pow_sub_one] - · grind + induction h <;> grind [mul_pow_sub_one] -- Another similar lemma lemma exp_larger' (n : ℕ) (h : 2 ≤ n) : (n - 2) * (n * (n - 1)) < (2 * n - 3) * 2 ^ (n - 1) := by