proposition: Lemma closure_eq0 (A : set T) : closure A = set0 -> A = set0.
proof: Proof. by move=> A0; apply/seteqP; split => //; rewrite -A0; exact: subset_closure. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed