This PR add constructors `.intCast k` and `.natCast k` to
`CommRing.Expr`. We need them because terms such as `Nat.cast (R := α)
1` and `(1 : α)` are not definitionally equal. This is pervaise in
Mathlib for the numerals `0` and `1`.
```lean
import Mathlib
example {α : Type} [AddMonoidWithOne α] : Nat.cast (R := α) 0 = (0 : α) := rfl -- not defeq
example {α : Type} [AddMonoidWithOne α] : Nat.cast (R := α) 1 = (1 : α) := rfl -- not defeq
example {α : Type} [AddMonoidWithOne α] : Nat.cast (R := α) 2 = (2 : α) := rfl -- defeq from here
-- Similarly for everything past `AddMonoidWithOne` in the Mathlib hierarchy, e.g. `Ring`.
```
f8cdb03352