This commit extends the week-04 proofs file with a substantial new Coq development covering recursive and tail-recursive definitions of addition and multiplication over naturals. It adds unit tests, fold/unfold lemmas, and machine-checked proofs that two addition implementations are equivalent, that addition is neutral/associative/commutative, and that four multiplication variants agree via accumulator-distribution lemmas. The multiplication-properties section is only partially completed, with several later theorems still marked Abort, but the file already establishes the main proof structure and reusable lemmas for future exercises. Practical effect: the repository now has a much richer formalization of arithmetic reasoning to build on.