dsimp doesn't visit numerals

Stream: lean4

[Jovan Gerbscheid]

It came up in #24492 that dsimp doesn't simplify numerals. The reason is that dsimp would end up in a loop if it visited the Nat argument of OfNat.ofNat {α : Type u} (x : Nat) [self : OfNat α x] : α, because raw nat literals are refolded. But the other two arguments are perfectly valid to dsimplify. This can be implemented with a dsimproc (in fact the not visiting numerals is already implemented via a dsimproc).