proposition: Lemma setU_sup s E: sub s (\Po E) -> least_upper_bound (subp_order E) s (union s).
proof: Proof. move=> sp. have [oi si1] := (subp_osr E). have su:sub (union s) E by apply: setU_s2; move=> y /sp /setP_P. have aux: sub s (substrate (subp_order E)) by ue. apply/(lubP oi aux); rewrite /upper_bound si1; split. split; first by apply/setP_P. move => y ys. have sy: sub y (union s) by apply: setU_s1. by apply/subp_gleP; split => //; move: (sp _ ys) => /setP_P. move=> z [zE hyp]; apply/subp_gleP; split => //; first by apply/setP_P. by apply: setU_s2 => y /hyp /subp_gleP [_ _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)