proposition: Lemma le_sum_all (P : pred T) (r : K) F G : \sum_(i in P) G i > 0 -> (forall i, P i -> G i > 0) -> (forall i, P i -> r <= F i / G i) -> r <= (\sum_(i in P) F i) / \sum_(i in P) G i.
proof: Proof. move=> HG HG' Hall. rewrite ler_pdivlMr // big_distrr /=. apply ler_sum => i Hi. by rewrite -ler_pdivlMr // ?Hall // HG'. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist