proposition: Lemma sup_setU (A B : set R) : has_sup B -> (forall a b, A a -> B b -> a <= b) -> sup (A `|` B) = sup B.
proof: Proof. move=> [B0 [l Bl]] AB; apply/eqP; rewrite eq_le; apply/andP; split. - apply sup_le_ub => [|x [Ax|]]; first by apply: subset_nonempty B0 => ?; right. by case: B0 => b Bb; rewrite (le_trans (AB _ _ Ax Bb)) // sup_ub //; exists l. - by move=> Bx; rewrite sup_ub //; exists l. - apply sup_le_ub => // b Bb; apply sup_ub; last by right. by exists l => x [Ax|Bx]; [rewrite (le_trans (AB _ _ Ax Bb)) // Bl|exact: Bl]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid