mathlib3

d673bafe - feat(topology/algebra/ordered): add lemmas, golf (#16343)

feat(topology/algebra/ordered): add lemmas, golf (#16343) * add lemmas about `nhds_within_Ici`/`nhds_within_Iic`; * move `order_separated` and `order_topology.to_order_closed_topology` up; * use new lemmas to golf some proofs.