proposition: Lemma set_of_upper_bounds_set0 r: Zo (substrate r) (upper_bound r emptyset) = substrate r.
proof: Proof. apply: extensionality; first by apply: Zo_S. move=> x xsr; apply /Zo_P; split=>//; split=>// y;case; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)