I'm currently trying to proof the following lemma in isabelle:
lemma helper:
fixes n :: nat
assumes "n ≥ 5"
shows "(n * n > 2*n + 1)"
proof (induction n)
qed
However the induction proof tactic forces me to show the following two cases:
1. 2 * 0 + 1 < 0 * 0
2. ⋀n. 2 * n + 1 < n * n ⟹ 2 * Suc n + 1 < Suc n * Suc n
With the first one obviously being wrong. However since my lemma states that it assumes n >= 5 I'm wondering why exactly it's not starting its induction for the base case n = 5? And since it doesn't do that, would also be interested in how I could get it to start induction at n = 5 instead of 0.