proposition: Lemma bounded_above_sub X Y r: sub Y X -> bounded_above r X -> bounded_above r Y.
proof: Proof. move=> YX [x ux]; exists x; apply: (sub_upper_bound ux YX). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)