proposition: Lemma Exercise1_23g r: order r -> cofinal (nregs_order r) (fun_image (substrate r) (canonical_reg_open r)).
proof: Proof. move=> or; red. move:(sub_osr (nreg_opens r)) => [pr1 pr2]. have ->:(substrate (nregs_order r) = nreg_opens r). by rewrite /nregs_order (proj2 (opp_osr pr1)). split. move=> t /funI_P [z zsr] ->; apply: Exercise1_23d2 => //. move=> x /Exercise1_23aP [ox [y yx]]. have ysr: inc y (substrate r) by move: ox => [[xsr _] _]; apply: xsr. move: (Exercise1_23d2 or ysr) => /Exercise1_23aP [p1 p2]. exists (canonical_reg_open r y); first by apply /funI_P;exists y. apply /Exercise1_23bP=> //; split => //; first by exists y. move: (ox) => [ox1 _]. rewrite /canonical_reg_open (Exercise1_22p or ox);apply: Exercise1_22j => //. apply: Exercise1_23c => //. move=> t /Zo_hi yt; move: ox1 => [_ h]; apply: (h _ _ yx yt). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)