This change reorganizes week-04_backward-and-forward-proofs.v for readers rather than altering the underlying proofs or definitions. It wraps auxiliary sections in hide markers and adds explicit exercise labels for the multiplication tasks, which should make the rendered material cleaner and easier for students to follow. The practical effect is better structure and readability in the teaching content, with no semantic change to the Coq development.