`RorQ` class in the Cauchy sequences / Bolzano-Weierstrass levels

[AlexKontorovich]

Problem: NormedField assumes the norm takes values in the reals, so is "begging the question" of the construction. Implement something like:

class ROrQ (K : Type*) extends LinearOrderedField K, Archimedean K where
  -- maybe add: DenselyOrdered, or FloorRing, depending on needs

with instances for R and Q being of this class.