proposition: Lemma finite_supportNe (I : choiceType) (P : set I) (F : I -> \bar R) : finite_support 0%E P (\- F)%E = finite_support 0%E P F.
proof: Proof. rewrite /finite_support !unlock; congr fset_set; congr setI. by rewrite seteqP; split=> x /= /eqP + /ltac:(apply/eqP); rewrite oppe_eq0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal