Theorem: List.pathLength_nonneg (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 head✝ : V
⊢ 0 ≤ [head✝].pathLength
Tactic:
simp [pathLength]
State after:
no goals