proposition: Lemma Rhull_involutive A : Rhull [set` Rhull A] = Rhull A.
proof: Proof. have [A0|/neitv_Rhull] := boolP (neitv (Rhull A)); first by rewrite set_itvK. by move=> ->; rewrite ?Rhull0 set_itvE Rhull0. 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