chore: use @[to_dual] in Bounds/Image (leanprover-community#35211)

This PR adds `@[to_dual]` annotations to primal theorems in `Mathlib.Order.Bounds.Image`, auto-generating their dual counterparts and deleting the hand-written versions. Covers `MonotoneOn`, `AntitoneOn`, `Monotone`, `Antitone`, `image2`, `IsCofinalFor`, `Prod`, and `Pi` sections.

[Diff relative to leanprover-community#35208](kim-em/mathlib4@kim/to-dual-bounds-basic...kim/to-dual-bounds-image)

- [x] depends on: leanprover-community#35208

🤖 Prepared with Claude Code

Author: kim-em