proposition: Lemma Exercise1_23i r x y: order r -> inc x y -> inc y (nreg_opens r) -> gle (nregs_order r) y (canonical_reg_open r x).
proof: Proof. move=> or xy. move /Exercise1_23aP => [h1 h2]. have ysr: (sub y (substrate r)) by move: h1 => [[ ok _] _]. move: (Exercise1_23d2 or (ysr _ xy)) => /Exercise1_23aP [h3 h4]. apply /(Exercise1_23bP or); split => //. rewrite (Exercise1_22p or h1). apply: (Exercise1_22j or (Exercise1_23c x or) (proj1 h1))=> t /Zo_P [tsr xt]. move: h1 => [[_ h] _]; apply: (h _ _ xy xt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)