∀ (K : Type u_2) [inst : Field K] (x : LaurentSeries.RatFuncAdicCompl K),
  (LaurentSeries.ratfuncAdicComplRingEquiv K) x =
    LaurentSeries.ratfuncAdicComplPkg.compare (LaurentSeries.LaurentSeriesPkg K) x