fix: disambiguate remaining duplicate Verso labels in Chapters 2, 5 and 9

[Chessing234]

The label collisions left in Chapters 2, 5 and 9 after #616, #624, #626, #634 and the Section 5.3/5.6 PRs:

Label	File	Count
Proposition 2.1.16 (recursive definitions).	2.1	2 (existence, uniqueness)
Proposition 2.3.6 (Multiplication preserves order)	2.3	2 (left, right)
Definition 2.3.11 (Exponentiation for natural numbers)	2.3	2 (the definition, the successor rule)
Example 5.1.10.	5.1	2
Definition 5.1.12 (bounded sequences)	5.1	2
Definition 5.2.3 (Eventually ε-close sequences)	5.2	2
Definition 5.2.6 (Equivalent sequences)	5.2	3
API for Example 5.5.2	5.5	2
Example 9.3.4, Example 9.3.5	9.3	2 each

Same convention as #624: definitions and propositions name the case in the parenthetical, examples take part letters (#634). Docstrings only.

Note on Section 2.2: it has two labels of the form (d) (Addition preserves order). Compare with Mathlib's {name}Nat.add_le_add_right`` that differ only in the Mathlib name they cite, so they are already distinct — left alone.

Checked: no duplicate one-line docstrings remain in any of the six files, all edited lines within 100 characters.

lake build of all six modules succeeds locally — Build completed successfully (3282 jobs).