proposition: Lemma greater_upper_bound x y X r: preorder r -> upper_bound r X x -> gle r x y -> upper_bound r X y.
proof: Proof. rewrite /lower_bound=> [] [rr _ tr] [xH h] yx. split; first order_tac. move=> z zX; apply: tr (h _ zX) yx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)