proposition: Lemma glb_set2 r x y z: order r -> gle r z x -> gle r z y -> (forall t, gle r t x -> gle r t y -> gle r t z) -> greatest_lower_bound r (doubleton x y) z.
proof: Proof. move=> or xz yz h. move:(arg2_sr xz) (arg2_sr yz) => xsr ysr. apply/(glbP or); first by move=>t /set2_P;case => ->. split;first by split; [order_tac | by move=>t /set2_P;case => ->]. move=> t [_ tb]; apply: h; apply: tb; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)