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