Theorem: SBtw.sbtw.symm (LeanCamCombi/MetricBetween.lean)

State before:
V : Type u_1
inst✝ : MetricSpace V
u v w : V
huv : u ≠ v
huw : u ≠ w
hvw : v ≠ w
d : Dist.dist u v + Dist.dist v w = Dist.dist u w
⊢ Dist.dist w v + Dist.dist v u = Dist.dist w u
Tactic:
simpa [dist_comm, add_comm] using d
State after:
no goals