Arithmetic normalisation of subtraction + SUC doesn't

[mn200]

If 0 < x is in the assumptions simp[] still won't prove f (SUC (x-1)) = f x

[mn200]

Though we might not want to normalise SUC x to x + 1 in general, in cases like this, where it will produce a substantial simplification. Perhaps SUC (x - n) for n any numeral should always simplify if the side-condition that n <= x can be proved.