Theorem: FltRegular.CaseI.two_lt (FltRegular/CaseI/AuxLemmas.lean)

State before:
p : ℕ
hpri : p.Prime
hp5 : 5 ≤ p
⊢ 2 < p
Tactic:
linarith
State after:
no goals