This removes checks in `Lean.Meta.reduceNat?` that caused it to fail on
terms it could handle because they contain meta variables in arguments.
This lead to those operations being reduced using their equational
definitions and slow performance on large patterns:
```
set_option profiler true
set_option profiler.threshold 1
def testMod (x:Nat) :=
match x with
| 128 % 1024 => true
| _ => false
-- elaboration took 3.02ms
def testMul (x:Nat) :=
match x with
| 128 * 1 => true
| _ => false
-- type checking took 11.1ms
-- compilation of testMul.match_1 took 313ms
-- compilation of testMul took 65.7ms
-- elaboration took 58.9ms
```
Performance is slower on `testMul` than `testMod` because `whnf` ends up
evaluateing `128 * 1` using Peano arithmetic while `128 % 1024` is able
to avoid that treatment since `128 < 1024`.
