ℝ and ℝ≥0 are *-ordered rings. #
Although the instance RCLike.toStarOrderedRing exists, it is locked behind the
ComplexOrder scope because currently the order on ℂ is not enabled globally. But we
want StarOrderedRing ℝ to be available globally, so we include this instance separately.
In addition, providing this instance here makes it available earlier in the import
hierarchy; otherwise in order to access it we would need to import
Mathlib/Analysis/RCLike/Basic.lean.