chore: remove stale comment

Author: plt-amy

src/Data/Rational/Base.lagda.md

@@ -557,13 +557,9 @@ reduceℚ : Ratio → Fraction
 reduceℚ (inc x) = split.choose x
 
 splitℚ : (x : Ratio) → fibre toℚ x
-splitℚ (inc x) = record
-  { fst = split.choose x
-  -- The use of 'recover' here replaces the calculated proof that
-  -- is-split-congruence returns by an invocation of Discrete-ℚ. This
-  -- has much shorter normal forms when applied to concrete values.
-  ; snd = ap inc (split.splitting x .snd)
-  }
+splitℚ (inc x) = record where
+  fst = split.choose x
+  snd = ap inc (split.splitting x .snd)
 
 abstract
   reduce-injective : ∀ x y → reduceℚ x ≡ reduceℚ y → x ≡ y