proposition: Lemma setI_i1 r x: interval r x -> x \cap (interval_uu r) = x.
proof: Proof. move=> hyp. have ->: interval_uu r = substrate r. apply: extensionality; first by apply: Zo_S. by move=> t tr; apply /Zo_P. suff: sub x (substrate r). move=> h; apply: extensionality; first by apply: subsetI2l. by move=> t tx; apply: setI2_i=>//; apply: h. case: hyp. case; first by move=> [a [b [_ _ _ ->]]] ; apply: Zo_S. case. move=> [a [b [_ _ _ ->]]]; apply: Zo_S. move=> [a [b [_ _ _]]]. case; move=> ->; apply: Zo_S. case; first by move=> [a _]; case; move=> ->; apply: Zo_S. case; first by move=> [a _]; case; move=> ->; apply: Zo_S. move=> ->; apply: Zo_S. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)