∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x y : K},
  0 ≤ ArchimedeanClass.mk x →
    0 ≤ ArchimedeanClass.mk y →
      ArchimedeanClass.stdPart (x * y) = ArchimedeanClass.stdPart x * ArchimedeanClass.stdPart y