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