# Proving a cumulative-product loop with a bounded result type — is there a standard idiom?

**URL:** https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715
**Category:** Help
**Tags:** spark
**Created:** [September 3, 2026, 12:59pm UTC](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715 "2026-09-03T12:59:24Z")
**Posts on this page:** 1
**Showing post:** 3

<div class="post-metadata">

### Author: ![damaki](https://forum.ada-lang.io/letter_avatar_proxy/v4/letter/d/3bc359/32.png) [@damaki](https://forum.ada-lang.io/u/damaki)
#### Post date: [September 3, 2026, 4:16pm UTC](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715/3 "2026-09-03T16:16:37Z")

</div>

Did you mean to duplicate your [other post?](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4713) kkson had already [replied there](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4713/2).

---

_[View the full topic](https://forum.ada-lang.io/t/proving-a-cumulative-product-loop-with-a-bounded-result-type-is-there-a-standard-idiom/4715)._