proposition: Lemma sub_Rhull (X : set R) : X `<=` [set x | x \in Rhull X].
proof: Proof. move=> x Xx/=; rewrite in_itv/=. case: (asboolP (has_lbound _)) => ?; case: (asboolP (has_ubound _)) => ? //=. + by case: asboolP => ?; case: asboolP => ? //=; rewrite !(lteifF, lteifT, sup_ub, inf_lb, sup_ub_strict, inf_lb_strict). + by case: asboolP => XinfX; rewrite !(lteifF, lteifT); [rewrite inf_lb | rewrite inf_lb_strict]. + by case: asboolP => XsupX; rewrite !(lteifF, lteifT); [rewrite sup_ub | rewrite sup_ub_strict]. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule