mathlib3

c82c2db1 - refactor(topology/instances/discrete): refactor the proof of `discrete_topology.order_topology_of_pred_succ` to show an equivalence (#16831)