proposition: Lemma cset0PN X : X != cset0 <-> X !=set0.
proof: Proof. rewrite cset0P; case: X => //= x Hx; split; last first. case=> a xa; apply/eqP => x0; move: xa; by rewrite x0. by case/set0P => /= d dx; exists d. 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