Using a definition in statement of lemma

Stream: general

[Quinn Culver]

How do I correctly use collinear in triangle_non_degen ? Seems like since the type of collinear is Prop, it should work as I have it.

import combinatorics.configuration
open configuration.projective_plane

open classical

universe u

variables {P L : Type u} [has_mem P L] [configuration.projective_plane P L]

variables (P L)
structure triangle :=
(p₀ p₁ p₂ : P)
(l₀ l₁ l₂ : L)
(i₀₁ : p₀ ∈ l₁)
(i₀₂ : p₀ ∈ l₂)
(i₁₀ : p₁ ∈ l₀)
(i₁₂ : p₁ ∈ l₂)
(i₂₀ : p₂ ∈ l₀)
(i₂₁ : p₂ ∈ l₁)

variables {P}
def collinear (p₀ p₁ p₂ : P) : Prop := ∃ l : L, p₀ ∈ l ∧ p₁ ∈ l ∧ p₂ ∈ l

lemma triangle_non_degen (T : triangle P L) (i₀₀ : T.p₀ ∉ T.l₀) :  collinear (T.p₀ T.p₁ T.p₂) :=  sorry

[Heather Macbeth]

@Quinn Culver collinear L T.p₀ T.p₁ T.p₂ should do it.

[Quinn Culver]

Thanks @Heather Macbeth. Give Antonella a big hug for me! :hug: