proposition: Lemma sup_pr a b r: order r -> inc a (substrate r) -> inc b (substrate r) -> has_supremum r (doubleton a b) -> [/\ gle r a (sup r a b), gle r b (sup r a b) & forall z, gle r a z -> gle r b z -> gle r (sup r a b) z].
proof: Proof. move=> or ast bsr hs. have sd: sub (doubleton a b) (substrate r) by apply: sub_set2. move: (supremum_pr or sd hs) => [[sr h1] h2]; split; try apply: h1; fprops. move=> z az bz; apply: h2. split; [by order_tac | by move=>y; case /set2_P => ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)