Ensure that `Nat.max` only `simpl`s if it does not result into a pattern match.

8 jobs for master in 8 minutes and 22 seconds (queued for 1 second)
Status Name Job ID Coverage
  Build
passed build-coq.8.7.0 #25465
fp

00:02:40

passed build-coq.8.7.1 #25464
fp

00:02:49

passed build-coq.8.7.2 #25463
fp

00:02:45

passed build-coq.8.8.0 #25462
fp-timing

00:02:40

passed build-coq.8.8.1 #25461
fp

00:02:51

passed build-coq.8.8.2 #25460
fp

00:02:55

passed build-coq.8.9.0 #25459
fp-timing

00:03:11

passed build-coq.dev #25458
fp

00:07:55