Commit 2019-11-24 23:02 a03a0720

chore(topology/metric_space/emetric_space): define edist_le_zero (#1735) This makes a few proofs slightly more readable.