feat(Order): add OrderType definitions

[YanYablonovskiy]

Adding the basic definitions around order types, the equivalence classes of linear orders under order isomorphism.

---

See draft discussion at #33420 and refactoring task #28278 .

• depends on: [Merged by Bors] - feat(Order): OrderIso involving Prod and Lex #33663
• depends on: [Merged by Bors] - feat: LinearOrder instance for Empty #31889

[github-actions]

PR summary 721b21cf2b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Order.Types.Defs (new file)	183

---

Declarations diff

+ OrderType
+ OrderType.instSetoid
+ ToType
+ _root_.RelIso.orderType_eq
+ bot_eq_zero
+ inductionOn
+ inductionOn₂
+ inductionOn₃
+ inhabited
+ instNeZeroOne
+ instOrdBot
+ instance : One OrderType
+ instance : Preorder OrderType
+ instance : Zero OrderType
+ liftOn
+ liftOn_type
+ nontrivial
+ not_lt_zero
+ omega0
+ one_ne_zero
+ pos_iff_ne_zero
+ type
+ type_eq
+ type_eq_one
+ type_eq_zero
+ type_le_type
+ type_le_type_iff
+ type_lt_type
+ type_ne_zero
+ type_ne_zero_iff
+ type_of_isEmpty
+ type_of_unique
+ type_toType
+ zero_le

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/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).

[github-actions]

🚨 PR Title Needs Formatting

Please update the title to match our commit style conventions.

Errors from script:

error: the PR title should be of the form
  abbrev: main title
or
  abbrev(scope): main title

Details on the required title format

The title should fit the following format:

<kind>(<optional-scope>): <subject>

<kind> is:

• feat (feature)
• fix (bug fix)
• doc (documentation)
• style (formatting, missing semicolons, ...)
• refactor
• test (when adding missing tests)
• chore (maintain)
• perf (performance improvement, optimization, ...)
• ci (changes to continuous integration, repo automation, ...)

<optional-scope> is a name of module or a directory which contains changed modules.
This is not necessary to include, but may be useful if the <subject> is insufficient.
The Mathlib directory prefix is always omitted.
For instance, it could be

• Data/Nat/Basic
• Algebra/Group/Defs
• Topology/Constructions

<subject> has the following constraints:

• do not capitalize the first letter
• no dot(.) at the end
• use imperative, present tense: "change" not "changed" nor "changes"

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(Order): OrderIso involving Prod and Lex #33663
• [Merged by Bors] - feat: LinearOrder instance for Empty #31889
  By Dependent Issues (🤖). Happy coding!

[vihdzp]

I believe this is redundant, this we're not in an @[expose] section. Likewise elsewhere.

Suggested change

@[no_expose]

[vihdzp]

Let's not name instances if we don't have to.

Suggested change

	instance instOrdBot : OrderBot OrderType where
	instance : OrderBot OrderType where