proposition: Lemma Exercise1_23e r x y: order r -> inc x (substrate r) -> inc y (substrate r) -> (inc y (canonical_reg_open r x) <-> forall z, gle r y z -> exists2 t, gle r z t & gle r x t).
proof: Proof. move=> or xsr ysr. rewrite /canonical_reg_open; split. move /setU_P=> [z yz] /Zo_P [] /setP_P zsr [[_ oz]]. move /(cofinal_inducedP or zsr) => [h1 h2]. move => t yt; move: (h2 _ (oz _ _ yz yt)) => [v v1 v2]. by move: v1 => /Zo_hi xv; exists v. move=> h; apply: Exercise1_22h => //. apply: Exercise1_23c => //. move=> z yz; move: (h _ yz) => [t zt xt]. exists t => //;apply: Zo_i=> //; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)