[Merged by Bors] - chore(Order/UpperLower/Principal): use to_dual

[JovanGerb]

This PR uses to_dual on intervals like UpperSet.Ici. The prerequisite file Order.Interval.Set.OrderIso is also tagged with to_dual.

---

[github-actions]

PR summary d1feaddbad

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

- IciBot
- Iic
- Iic_iInf
- Iic_iInf₂
- Iic_inf
- Iic_inj
- Iic_injective
- Iic_le
- Iic_ne_Iic
- Iic_ne_bot
- Iic_sInf
- Iic_strictMono
- Iic_top
- Iio
- Iio_bot
- Iio_eq_bot
- Iio_strictMono
- Ioi_le_Ici
- bot_lt_Iic
- coe_Iic
- coe_Iio
- image_Ici
- image_Ico
- image_Ioi
- map_Iic
- map_Iio
- mem_Iic_iff
- mem_Iio_iff
- preimage_Ici
- preimage_Ioc
- preimage_Ioi

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[bryangingechen]

Thanks!
bors r+

[mathlib-bors]

This PR was included in a batch that was canceled, it will be automatically retried

[mathlib-bors]

Build failed (retrying...):

• ci (staging) / Build

[mathlib-bors]

Build failed (retrying...):

• ci (staging) / Post-Build Step

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Lint style
• ci (staging) / Post-CI job