proposition: Lemma Exercise1_23bP r : order r -> forall X Y, (gle (nregs_order r) X Y <-> [/\ nonempty X, nonempty Y, open_r r X, open_r r Y & sub Y X]).
proof: Proof. move=> or X Y; split. by move /opp_gleP /sub_gleP => [] /Exercise1_23aP [pa pb] /Exercise1_23aP [pc pd] pe. by move => [pa pb pc pd pe]; apply /opp_gleP /sub_gleP; split => //;apply /Exercise1_23aP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)