Fix the Rocq statements of 1962 A2, A6 and B5 (#358)

[yaqub1971]

This PR corrects the three defective Rocq statements reported in #358 (items 1–3). Only the mathematical content of the statements changes; imports, preamble and formatting are left exactly as upstream.

coq/src/putnam_1962_b5.v — the lower bound was encoded as (3 * (n%:R + 1) + 1) / (2 * n%:R + 2), i.e. (3n+4)/(2n+2), which is false at n = 2 (it asserts 5/3 < 5/4). It is now (3 * n%:R + 1) / (2 * n%:R + 2), i.e. (3n+1)/(2n+2), the bound of the problem and of the Lean and Isabelle statements.

coq/src/putnam_1962_a6.v — in hSScond, the second conjunct ~(A r \/ A (-r)) becomes ~(A r /\ A (-r)) (as written, it made the hypotheses contradictory and the theorem provable in one line), and the three occurrences of r = 0 (Leibniz equality on non-canonical Q fractions, e.g. 0#2 <> 0) become r == 0 (Qeq). With these changes the hypotheses are satisfied by the positive rationals.

coq/src/putnam_1962_a2.v — putnam_1962_a2_solution contained only the family a / (1 - c * x) ^ 2, but the statement's own condition P is also satisfied by other functions (e.g. the indicator of {0}, whose integral over every [0, x] is 0), so the theorem was false. The definition now has the four-case solution set of the Lean statement of the same problem, transcribed to Rocq; the theorem itself is unchanged.

Verification: the corrected statements compile on Coq 8.18.0 / MathComp 2.1.0 / MathComp-Analysis 1.0.0 and, with the compatibility lines described in #358 §4, on Rocq 9.1.0 / MathComp 2.5 / MathComp-Analysis 1.16.0. Machine-checked proofs of all three corrected statements (and derivations of False / vacuity from the unmodified originial ones) are in https://github.com/yaqub1971/PutnamBench_ROCQ, as referenced by the leaderboard entry added in #359.

[GeorgeTsoukalas]

Looks great, thanks! Feel free to merge. (Actually I merged)

[yaqub1971]

Thanks. Issue #358 has been closed and resolved.