mathlib3

feat(combinatorics.simple_graph.metric): `enat` valued dist function on graphs

#18692

Open