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

[damaki]

Did you mean to duplicate your other post? kkson had already replied there.