proposition: Lemma Exercise1_22a u1 u2: open_o r u1 -> open_o r u2 -> open_o r (u1 \cup u2).
proof: Proof. move=> [u1p u1r][u2p u2r]; split. move=> t; case/setU2_P; [apply: u1p | apply: u2p]. by move=> x y;case/setU2_P; move=> h le; apply /setU2_P; [left; apply: (u1r x) | right; apply: (u2r x)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)