proposition: Lemma Exercise1_23f r x y: order r -> gle r x y -> gle (nregs_order r) (canonical_reg_open r x) (canonical_reg_open r y).
proof: Proof. move=> or xy. have xsr: (inc x (substrate r)) by order_tac. have ysr: (inc y (substrate r)) by order_tac. move: (Exercise1_23d2 or xsr) (Exercise1_23d2 or ysr) => s1 s2. apply /opp_gleP /sub_gleP;split => //. apply: Exercise1_22j; (try apply: Exercise1_23c) => //. move=> t => /Zo_P [tsr yt]; apply /Zo_i => //; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)