proposition: Lemma Exercise1_22n: open_r r (substrate r).
proof: Proof. split. split; fprops; move=> x y _ xy; order_tac. by move=> v [v1 _] [];rewrite iorder_sr // => h _; apply: extensionality. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)