proposition: Lemma Exercise1_22f u: open_o r u -> sub (open_bar r u) (substrate r).
proof: Proof. move=> [ou1 ou2] t => /setU_P [y ty] /Zo_P [] /setP_P ysr _. by apply: ysr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)