Theorem: NotCollinear.rotate (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₂ : {v, w, u} ⊆ l
⊢ {u, v, w} ≤ {v, w, u}
Tactic:
simp
State after:
no goals