Theorem: NotCollinear.swap (LeanCamCombi/SylvesterChvatal.lean)

State before:
V : Type u_1
inst✝² : MetricSpace V
u v w : V
inst✝¹ : Finite V
inst✝ : Nontrivial V
x y z : V
h : NotCollinear u v w
l : Set V
h₁ : l.IsLine
h₂ : {w, v, u} ⊆ l
⊢ {u, v, w} ≤ {w, v, u}
Tactic:
simp
State after:
no goals