proposition: Lemma closureE A : closure A = smallest closed A.
proof: Proof. rewrite eqEsubset; split=> [x ? B [cB AB]|]; first exact/cB/(closure_subset AB). exact: (smallest_sub (@closed_closure _ _) (@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