Explain Proof — Development skill for Claude Code

Walk through a completed Coq proof tactic by tactic, explaining each step in plain English with mathematical intuition, showing how the proof state evolves, and summarizing the overall proof strategy. This command is read-only — it never modifies source files.

The user provides a target proof in one of these forms:

• A lemma or theorem name (e.g., plus_comm)
• A file path and line number (e.g., Arithmetic.v:42)
• No argument, meaning "the proof I'm currently looking at" — use surrounding c