Commit 2025-03-18 12:49 4d4e085b
View on Github →chore: use to_additive for BoundedAdd (#23009)
BoundedAdd and BoundedMul results were in separate section of the file that defines them, with very similar proofs.
This PR uses to_additive to generate the Add results from the Mul results, and also adds an instance for the Mul case, that was present only for Add.