Dustin Bryant (Jan 09 2023 at 20:47): Dustin Bryant (Jan 09 2023 at 20:47):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?
Dustin Bryant (Jan 09 2023 at 21:13):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 27 2024 at 01:05 UTC