Compress Proof

Description

Given a working Coq proof, systematically search for shorter or cleaner alternatives using hammer tactics, lemma search, and tactic chain simplification. Present verified alternatives ranked against the original. Never modify the original file unless the user explicitly chooses a replacement. ## Identify the target proof The user will specify a proof by name (e.g., `my_lemma`), by file location (e.g., `src/Foo.v:42`), or by asking you to compress the proof at point in the current context. If t

Installation

Installs to ~/.claude/skills/ekirton-poule-compress-proof/SKILL.md

Restart Claude Code, or start a new session, for it to be picked up.