mathlib

bf229dd5 - feat(topology/metric_space/basic): dist_ne_zero (#7552)