proposition: Lemma closure_id E : closed E <-> E = closure E.
proof: Proof. split=> [?|->]; last exact: closed_closure. rewrite eqEsubset; split => //; 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