chore(Data/NNReal/Defs): fix LinearOrderedCommGroupWithZero on ℝ≥0 (leanprover-community#40208)

This PR was automatically created from PR leanprover-community#36911 by @jjdishere via a [review comment](leanprover-community#36911 (comment)) by @faenuccio.

Co-authored-by: jjdishere <107380768+jjdishere@users.noreply.github.com>

Author: 2 people

Mathlib/Data/NNReal/Defs.lean

@@ -115,9 +115,14 @@ noncomputable instance : Semifield ℝ≥0 := fast_instance%
     rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
     (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ => rfl)
 
-noncomputable section
-deriving instance LinearOrderedCommGroupWithZero for NNReal
-end
+instance : IsOrderedRing ℝ≥0 :=
+  Nonneg.isOrderedRing
+
+instance : IsStrictOrderedRing ℝ≥0 :=
+  Nonneg.isStrictOrderedRing
+
+noncomputable instance : LinearOrderedCommGroupWithZero ℝ≥0 where
+  bot_le h := h.2
 
 example {p q : ℝ≥0} (h1p : 0 < p) (h2p : p ≤ q) : q⁻¹ ≤ p⁻¹ := by
   with_reducible_and_instances exact inv_anti₀ h1p h2p