proposition: Lemma decompN0 (A : set rT) : decomp A != set0.
proof: Proof. rewrite /decomp; case: ifPn => [_|AN0]; first by apply/set0P; exists set0. case: pselect=> //= Am; last by apply/set0P; exists A. case: cid=> //= D [_ _ _ _ Aeq]; apply: contra_neq AN0; rewrite Aeq => ->. by rewrite bigcup_set0. 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)