proposition: Lemma le_Rhull : {homo (@Rhull R) : A B / (A `<=` B) >-> {subset A <= B}}.
proof: Proof. move=> A B AB; suff: [set` Rhull A] `<=` [set` Rhull B] by []. rewrite Rhull_smallest; apply: smallest_sub; first exact: interval_is_interval. by rewrite Rhull_smallest; apply: sub_smallest. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) HB(structures) reals ereal signed topology normedtype sequences