no goals
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
l : L
⊢ 2 < pointCount P l
simpa only [pointCount_eq P l, Nat.succ_lt_succ_iff] using one_lt_order P L