prove-plus-comm
Guide for completing Coq proofs involving arithmetic properties like addition commutativity. This skill should be used when working on Coq proof files that require proving properties about natural number arithmetic using induction, particularly when lemmas like plus_n_O and plus_n_Sm are involved.
npx skills add majiayu000/claude-skill-registry --skill prove-plus-comm-letta-ai-skills-2 --agent claude-code
Same command for any agent — swap --agent for codex, cursor, copilot.
Weekly change comes from our own snapshots, not the repository page — it measures attention, not adoption.
# Coq Arithmetic Proof Completion This skill provides guidance for completing Coq proofs involving arithmetic properties on natural numbers, particularly addition commutativity and related lemmas. ## When to Use - Completing incomplete Coq proofs about natural number arithmetic - Proving commutativity, associativity, or other properties of addition - Working with induction on natural numbers in Coq - Debugging proofs that use standard library arithmetic lemmas ## Approach ### 1. Understand the Proof Structure Before modifying any proof: 1. Read the entire proof file to understand what is being proven 2. Identify the theorem statement and its type signature 3. Note any auxiliary lemmas that are defined or imported 4. Locate the incomplete portions (often marked with `Admitted` or `(* TODO *)`) ### 2. Analyze the Proof State For inductive proofs on natural numbers: - **Base case (n = 0)**: After `simpl`, identify what remains to be proven - **Inductive case (n = S n')**: Note the inductive hypothesis name (typically `IHn'`) and what goal remains after simplification To understand goal states: - Use `Show.` or inspect after `simpl.` to see current goals - Recognize that `0 + m` simpli
- When to Use
- Approach
- 1. Understand the Proof Structure
- 2. Analyze the Proof State
- 3. Apply Standard Lemmas
- 4. Rewrite Direction Convention
- 5. Standard Proof Pattern for Addition Commutativity
- Verification Strategy
- Common Pitfalls
- Wrong Rewrite Direction
- Missing Lemma Import
- Incorrect Induction Variable
- Forgetting to Apply Inductive Hypothesis
- Definition vs Lemma Confusion
What does the prove-plus-comm skill do?
Guide for completing Coq proofs involving arithmetic properties like addition commutativity. This skill should be used when working on Coq proof files that require proving properties about natural number arithmetic using induction, particularly when lemmas like plus_n_O and plus_n_Sm are involved.
How do I install it?
Run `npx skills add majiayu000/claude-skill-registry --skill prove-plus-comm-letta-ai-skills-2 --agent claude-code` — it drops the skill into your project so the agent can pick it up. Swap the --agent value for codex, cursor or copilot if you use one of those.
Where does this skill come from?
From majiayu000/claude-skill-registry, a repository with 534 stars. We read it straight from the repository tree rather than a submitted listing, so what you see here is what is actually published.
Is a popular skill a good skill?
Not necessarily. Stars measure attention, not adoption — a repository can trend for a week and be abandoned. That is why we show the weekly change from our own snapshots next to the total, instead of a single flattering number.