proposition: Lemma sup_inclusion A x y: sub x A -> sub y A -> least_upper_bound (subp_order A) (doubleton x y) (x \cup y).
proof: Proof. move=> xA yA. have sd: (sub (doubleton x y) (\Po A)) by apply: sub_set2; apply/setP_P. apply: (setU_sup sd). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)