proposition: Lemma big_fset_subset (I J : {fset T}) (F : T -> R) : (forall x, 0 <= F x) -> {subset I <= J} -> \sum_(i : I) F (val i) <= \sum_(j : J) F (val j).
proof: Proof. move=> ge0_F le_IJ; rewrite !big_fset_seq /=. rewrite [X in _<=X](bigID [pred j : T | j \in I]) /=. rewrite ler_wpDr ?sumr_ge0 // -[X in _<=X]big_filter. rewrite le_eqVlt; apply/orP; left; apply/eqP/perm_big. apply/uniq_perm; rewrite ?filter_uniq //; last move=> i. rewrite mem_filter; case/boolP: (_ \in _) => //=. by move/le_IJ => ->. Qed.
imports: mathcomp(all_ssreflect all_algebra)