do you want a small contribution to mathlib

Stream: general

[Huỳnh Trần Khanh]

hmm... I think x_le_sum and sum_le_x are pretty useful to other people too... would you want to include these lemmas in mathlib? https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20orange.20bar.20hell!/near/262929724

[Huỳnh Trần Khanh]

my proposed name for sum_le_x would be sum_le_upper_bound_mul_length

[Huỳnh Trần Khanh]

hmm wait is there already a mathlib lemma for that? I don't want to add duplicate stuff

[Mario Carneiro]

It looks like it follows from stuff like the sum of a constant sequence is l.length * a and sums are monotonic

[Mario Carneiro]

if you can state these results over finset sum then they almost certainly exist already; for lists the theory is less robust but I would still go at it from this angle