proposition: Lemma Exercise1_23d2 r x: order r -> inc x (substrate r) -> inc (canonical_reg_open r x) (nreg_opens r).
proof: Proof. move=> or xsr; apply /Exercise1_23aP; split. move: (Exercise1_23c x or) => aux; apply: Exercise1_22i => //. by exists x; apply: Exercise1_23d1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)