proposition: Lemma supremum_setU1 a b: sub a E -> has_supremum r a -> inc b E -> supremum r (a +s1 b) = sup r (supremum r a) b.
proof: Proof. move=> asr hsa bsr; move: lr => [or _]; symmetry; apply: supremum_pr2 =>//. by apply: lattice_finite_sup1 => //;apply: supremum_pr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)