fix: `constructorApp'?` on `Nat` offsets `s + 0`

This PR fixes the internal error `mkNoConfusion: No manifest constructors` in `contradiction` on hypotheses such as `h : 0 + 0 = 1`.

`constructorApp'?` and `isConstructorApp'?` returned `none` for every offset term `s + 0`, but `s + 0` reduces to `s`, which may be a constructor application. They now fall through to the regular `whnf`-based path in this case.

Closes #16285

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>