proposition: Lemma hull_eq0 X : (hull X == set0) = (X == set0).
proof: Proof. apply/idP/idP=> [/eqP abs|]; last by move=> /eqP ->; rewrite hull0. apply/negPn/negP => /set0P[/= d] => dX. move: abs; rewrite funeqE => /(_ d); rewrite propeqE /set0 => -[H _]; apply H. exact/subset_hull. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist