Agent Skills: prove-plus-comm

Guidance for proving mathematical properties in Coq using induction, specifically addition commutativity and similar arithmetic lemmas. This skill should be used when working with Coq proof assistants to complete induction proofs, fill in proof cases, or apply standard library lemmas like plus_n_O and plus_n_Sm.