proposition: Lemma sub_upper_bound x X Y r: upper_bound r X x -> sub Y X -> upper_bound r Y x.
proof: Proof. rewrite /lower_bound=> [] [xR lo] YX. split=>//; move=> y yY; apply: lo (YX _ yY). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)