OpenMath Rocq Theorem

Instructions

Set up the Rocq proving environment, validate opam switches, and prove downloaded OpenMath theorems. Assumes the theorem workspace was already created by the openmath-open-theorem skill.

This skill package is self-contained: it consists of this SKILL.md plus the local references/ files in this directory. It does not bundle or install sibling rocq-* companion skills.

Workflow checklist

• Environment: Verify rocq (or coqc), dune, and opam are installed and the active opam switch matches the project's .opam-switch or opam file. See the rocq-setup skill for installation and switch management.
• Companion skills: If companion Rocq skills such as rocq-proof, rocq-ssreflect, rocq-setup, or rocq-dune are already installed in the active agent, use them. See references/companions.md for when each one is useful. This isolated package does not include their code and does not install them for you.
• Preflight: Confirm the environment is healthy before proving: