proposition: Lemma lub_set2 r x y z: order r -> gle r x z -> gle r y z -> (forall t, gle r x t -> gle r y t -> gle r z t) -> least_upper_bound r (doubleton x y) z.
proof: Proof. move=> or xz yz h. move:(arg1_sr xz)(arg1_sr yz) => xsr ysr. apply/(lubP 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)