What's going on in this proof is that simpl is unfolding both decode_nat and decode, even though decode is marked simpl never. This is a bug in Coq and std++ should not rely on it.
Alternate take on https://gitlab.inria.fr/bertot/stdpp/-/commit/895121f919c6f1332f41f658ce7f850e391eb49e, which is used as an overlay in Coq for https://github.com/coq/coq/pull/13448.