proposition: Lemma inf_setU (A B : set R) : has_inf A -> (forall a b, A a -> B b -> a <= b) -> inf (A `|` B) = inf A.
proof: Proof. move=> hiA AB; congr (- _). rewrite image_setU setUC sup_setU //; first exact/has_inf_supN. by move=> _ _ [] b Bb <-{} [] a Aa <-{}; rewrite lerNl opprK; apply AB. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid