proposition: Lemma decomp_finite_set (A : set rT) : finite_set (decomp A).
proof: Proof. rewrite /decomp; case: ifPn => // A0; case: pselect => // X. by case: cid => /= ? []. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)