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
.