Wire the Rocq backend into the proof agent

[dingf3ng]

Summary

• run the proof agent end to end through ProverBackend and the Rocq adapter
• remove the legacy CoqInterface runtime and test path
• expose only Rocq in this independently testable stack tip
• add controller, CLI, rendering, cleanup, and real prover workflow coverage

Stack dependency

Draft; depends on #4. The narrow wiring-only diff is available in the fork at dingf3ng#5. Until the lower PRs merge, GitHub shows their commits here as well.

Verification

• 92 deterministic tests passed; the real Rocq agent workflow passed in 7.27s.
• No Python reference to CoqInterface or either unrelated adapter remains.