proposition: Lemma Exercise1_22s1P x: inc x (substrate (reg_open_order r)) <-> open_r r x.
proof: Proof. rewrite /reg_open_order (proj2 (sub_osr (reg_opens r))). split; [ by move /Zo_hi | apply:reg_opens_i ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)