proposition: Lemma lt0_mset (U : set T) (r : R) : (r < 0)%R -> mset U r = set0.
proof: Proof. move=> r0; apply/seteqP; split => // x/=. by apply/negP; rewrite -leNgt (@le_trans _ _ 0)// lee_fin ltW. 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)