Piecewise larger list means larger sum

Stream: Is there code for X?

[Aatman Supkar]

Is there a theorem which proves that given a L1 L2 : List α of the same length where LinearOrder α can be inferred, if L1.get(i) ≥ L2.get(i) for all i, then List.sum L1 ≥ List.sum L2?

[Aaron Liu]

docs#List.sum_le_sum might be helpful

[Aaron Liu]

You can use docs#List.finRange_map_get along with docs#List.sum_le_sum to prove this