feat(temperature): PositiveTemperature refactor

[ichxorya]

At this first commit, I would follow the suggestion of @jstoobysmith to break the PR down into pieces. Hopefully this could be reviewed as a passing commit 😄

However, note that at this point, the Basic.lean file only contain:

• Temperature and PositiveTemperature definitions: type conversions, ext lemma, linear order and relevant order/comparison lemmas.
• Beta and Inverse Beta (ofBeta) was moved from Temperature to PositiveTemperature, with additional lemmas in their antimonotonicity (T1 > T2 <=> Beta T1 < Beta T2, ect.)

---

For the rest (derivatives, limits, ect.), I have also proved them following the PositiveTemperature refactor here (https://github.com/SEhumantics/PhysLean/tree/feat/nghiabt/postemp/PhysLean/Thermodynamics/Temperature). However, I can only commit more until further acceptance from maintainer revisions!

---

Referred issues: #861 #860 - #892 (directly dependent on the Beta and Inverse Beta functions)

[jstoobysmith]

Hey, when you are ready for this to be reviewed, could you unmark it as a draft?

[ichxorya]

Hey, when you are ready for this to be reviewed, could you unmark it as a draft?

Yes I think it is ready, but I marked as draft since it's not ready to be merge. Can you please review this section first? I'd like to add the rest of the original Basic.lean but it would be too lengthy for now.