proposition: Lemma Exercise1_23d1 r x: order r -> inc x (substrate r) -> inc x (canonical_reg_open r x).
proof: Proof. move=> or xsr; apply: Exercise1_22e => //; first by apply: Exercise1_23c. by apply: Zo_i => //; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)