There is limited support for handling multiplication in constraint-solving.
Heres is an example:
It proves the following identities:
2*(1+2+…+n) = n(n+1)
6*(1^2 + 2^2 + … + n^2) = n*(n+1)(2n+1)
…
66*(1^10 + 2^10 + … + n^10) = some-polynomial-of-degree-11
In general, only equalities involving multiplication can be handled
automatically.
Inequalities cannot be handled.
Using MUL to handle multiplication manually in proof construction is very
labor-intensive,
and it should be avoided whenever possible.