I want to efficiently show that int(Sum Nats_Here_indexed_by_some_list) = Sum (int(Nats_Here_indexed_by_some_list)) where Nats_Here_indexed_by_some_list is a natural number which does NOT feature subtraction. The upper bound for the sum is the length of the list I am using to sum, and I discovered I can prove this by induction but this feels inefficient. Surely there is a well-suited lemma for this?
I was looking for "of_nat_sum". For some reason it didn't previously call this lemma. I'm not sure how to close this out here.....
Last updated: Apr 02 2025 at 01:40 UTC