proposition: Lemma sup_comparable r x y: gle r x y -> order r -> least_upper_bound r (doubleton x y) y.
proof: Proof. move=> xy or; apply: lub_set2 =>//;order_tac; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)