Fix divstep postconditions in generated APIs

[JasonGross]

Summary

• correct the divstep true-branch postcondition to specify r - v for the fifth output
• restore the missing validity bound for the fourth output
• tie the exported contract to the canonical Bernstein–Yang arithmetic specification with a focused Rocq regression lemma
• regenerate the 94 affected C, Rust, Go, Java, and Zig files

All generated-file changes are limited to the two corrected documentation lines; function bodies are unchanged.

Tests

• opam exec -- make -j16 SKIP_BEDROCK2=1 src/COperationSpecifications.vo
• rebuilt src/ExtractionOCaml/word_by_word_montgomery and regenerated all affected files
• compiled all changed C files with -Wall -Wpedantic -Werror
• cargo build in fiat-rust
• zig build in fiat-zig
• verified all 94 generated contracts contain arg5 - arg4 and an out4 validity bound, with no remaining arg4 - arg4 contract

Go and Java toolchains were unavailable locally; their generated files were covered by regeneration and exact contract checks.

Fixes Scrutineer finding #2522.

Authorship note: this was researched and written by an AI coding agent
(OpenAI Codex), working on Jason Gross's behalf; Jason reviews what is
posted from this account.