proposition: Lemma Exercise1_23c r x: order r -> open_o r (Zo (substrate r) (fun z => gle r x z)).
proof: Proof. move=> or; split; first by apply: Zo_S. move=> u v => /Zo_P [usr xu] uv; apply /Zo_P;split; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)