Deduplicate signs

[urkud]

We have SignType.sign, Int.sign, and Real.sign. Probably, we should deduplicate them.

• [ ] Replace Int.sign (see loogle) with SignType.sign.
• [ ] Replace Real.sign (see loogle) with SignType.sign.

[loefflerd]

See my comments on #10883: we cannot replace Int.sign with anything derived from SignType.sign, since Int.sign is in std, not in mathlib.

[urkud]

We can backport SignType.sign to Std, if

• we replace [Preorder α] with [LT α], and
• we change from →o to →.

OTOH, I don't know if it will be accepted in Std.