#411 Manual rewriter for arithmetic on constants

[Guillaume Verdier]

In a proof, if there are some arithmetic operations on constants, there is no easy way to apply the operations. We should have a manual rewriter to be able to click on the operators when the operands are constants in order to apply them (e.g., replace 1 + 1 by 2).
We do not want this to be done by an automatic rewriter because reducing the operations is not always the right call (for example, if we have x + 1 = y and x + 1 + 1 in another hypothesis, we want to be able to rewrite it into y + 1, which would not be possible if a reasoner automatically replaces it by x + 2).