proposition: Lemma Exercise1_22rP u v: gle (reg_open_order r) u v <-> [/\ open_r r u, open_r r v &sub u v].
proof: Proof. split; first by move /sub_gleP => [] /Zo_hi pa /Zo_hi pb pc. by move=> [p1 p2 p3]; apply /sub_gleP => //; split => //; apply:reg_opens_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)