proposition: Lemma glb_set0 r: order r -> forall x, greatest_lower_bound r emptyset x = greatest r x.
proof: Proof. move=> or; rewrite /greatest_lower_bound set_of_lower_bounds_set0. by rewrite /greatest_induced iorder_substrate. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)