wasm-to-v: document the `%N` scope recipe for mathcomp consumers of emitted `.v`

[0xGeorgii]

Problem

Emitted .v files spell every N literal with the standard-library scope key: 0%N, 1%N (indices, reach_func, reach_visible_locs, Ma arguments). Under vanilla Rocq this is correct and the standalone coqc gate elaborates it as-is.

Under mathcomp, however, ssrnat re-delimits %N to nat_scope (and provides %num as its replacement key for BinNat's N_scope). Any consumer that imports ssrnat before using the emitted definitions silently reinterprets 1%N : N as 1%N : nat and fails with type errors at the record fields.

Hit while discharging the emitted reachability obligations in wasm-verifier (Inference-Global-Software/wasm-verifier#42). The working consumer recipe is one line placed after the mathcomp imports:

Local Delimit Scope N_scope with N.

(Local matters — a file-global Delimit leaks to every file that Requires it and re-breaks %N there in the other direction.)

Why not just emit %num

%num is defined by ssrnat — it does not exist in a mathcomp-free context, so switching the emission would break the standalone contract and the repo's own coqc gate (which elaborates against the stub with no mathcomp). %N is the right key for what the emitter targets.

Proposed resolution

Document the recipe rather than change the emission: add a short "mathcomp consumers" note to core/wasm-to-v/ROCQ_CONTRACT.md (the required-context section) covering both accommodations discovered during the discharge — the Local Delimit Scope N_scope with N. line, and importing ssreflect after the emitted definitions until #412 (the Ma of al binder) is fixed, after which import order stops mattering.

Found during the downstream discharge for #354 / #411; both discharged examples in wasm-verifier PR #42 use exactly this recipe.