proposition: Lemma bounded_both_sub X Y r: sub Y X -> bounded_both r X -> bounded_both r Y.
proof: Proof. move => YX [p1 p2]. split; [ apply: (bounded_above_sub YX p1) | apply: (bounded_below_sub YX p2)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)