This commit introduces a substantial Coq worksheet centered on “mystery functions,” with formal specifications over naturals, booleans, tuples, and trees, plus example implementations and partial proof scripts. It looks like teaching or lab material: students are guided to identify functions from algebraic properties, write unit tests, and prove soundness or uniqueness where possible. The file adds real instructional content rather than boilerplate, and it expands the project with a reusable set of proof exercises and examples. Practically, it gives contributors a new verified-programming exercise set to work through.