Theorem: Delta_comm (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 u v w : V
⊢ Delta u v w = Delta w v u
Tactic:
simp only [Delta, add_comm, dist_comm]
State after:
no goals