proposition: Lemma Exercise1_22s: greatest (reg_open_order r) (substrate r).
proof: Proof. move: (Exercise1_22n) => so. split; first by apply /Exercise1_22s1P. move=> x => /Exercise1_22s1P ox; move: (proj1 (proj1 ox)) => xsr. apply /Exercise1_22rP;split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)