Unnecessary reduction of nosimpl wrapper

[llelf]

Description of the problem

From Coq Require Import ssreflect. (* for nosimpl and if-is notation *)
(* NB: nosimpl ≡ Notation nosimpl t := (let: tt := tt in t). *)

Fixpoint foo (n : nat) : nat := if n is S n' then foo n' else S n.
Definition add := nosimpl Nat.add.

Goal forall m n, 0 <> foo (add (S m) n). simpl.
(* Expected: forall m n : nat, 0 <> foo (add m n)
   Actual:   forall m n : nat, 0 <> foo (m + n)
*)
Abort.

A slightly less silly and more real-world example:

From mathcomp Require Import ssreflect ssrbool ssrnat.

Fixpoint fib (n : nat) : nat :=
  if n is (n''.+1 as n').+1 then fib n'' + fib n' else n.
Arguments fib n : simpl nomatch.

Goal forall m n, 0 <= fib (m.+1 + n).+1. move=> /=.
(* Unexpected, but actual:
     forall m n : nat, 0 <= fib (m + n)%Nrec + fib (m.+1 + n) *)
Abort.

Coq Version

8.9.1, 8.10+β3, master

[llelf]

TIL:

From mathcomp Require Import ssreflect ssrnat.

Lemma addnAC a b c : a + b + c = a + c + b.    (* addn *)
by rewrite -> PeanoNat.Nat.add_shuffle0.       (* Nat.add *)
Qed.

Check PeanoNat.Nat.add_shuffle0 : forall a b c, _ = (_ + _)%nat.
Check PeanoNat.Nat.add_shuffle0 : forall a b c, _ = (_ + _)%coq_nat.