Document the %N scope recipe for mathcomp consumers of emitted .v (#413)

[0xGeorgii]

Fixes #413. Stacked on #414 (base is 412-ma-ofs-binder); this PR contains only the documentation commit.

Adds a "mathcomp consumers" subsection to ROCQ_CONTRACT.md's required-context section covering what the downstream discharge (Inference-Global-Software/wasm-verifier#42) discovered:

• the Local Delimit Scope N_scope with N. recipe, placed after the mathcomp imports, with the mechanism: mathcomp's ssrnat rebinds the %N key to nat_scope (keeping %num as its replacement key for BinNat's N_scope), so an ssrnat-importing consumer re-reads 1%N : N as nat and fails at the record fields. Also why Local matters (a file-global Delimit leaks through Require), the default-on hiding-delimiting-key warning, and the symmetric cost (mathcomp's %N-keyed nat notations stop parsing in that file)
• why the emitter stays on %N rather than emitting %num: that key is defined by ssrnat, so it does not exist in the mathcomp-free context the standalone contract and the repo's own coqc gate target
• the import-order accommodation recorded as historical: gone as of the Ma ofs rename (wasm-to-v: rename the emitted Ma helper's of binder (reserved by ssreflect) #412), needed only for a .v generated before it; with the residual noted that emitted Definition names are user identifiers printed verbatim, so a source function named of would reintroduce the collision for its own line

Claims verified against primary sources (mathcomp 2.6.0 boot/ssrnat.v L136-138 for the two Delimit lines; rocq ssrparser.mlg's ssrbinder grammar for the of keyword) and replayed locally against Rocq 9.2 by simulating ssrnat's Delimit sequence.

Confidence Score: 5/5

The documentation-only PR appears safe to merge.

No blocking failure remains.

Important Files Changed

Filename	Overview
core/wasm-to-v/ROCQ_CONTRACT.md	Documents %N scope rebinding for mathcomp consumers and the historical ssreflect import-order accommodation.
CHANGELOG.md	Adds a changelog entry describing the new mathcomp-consumer guidance.

_{Reviews (2): Last reviewed commit: "Document the %N scope recipe for mathcom..." | Re-trigger Greptile}

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!