{R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring S] →
      [inst_1 : PartialOrder S] →
        {R' : Type u_3} →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring R'] → [Algebra R R'] → (v : AbsoluteValue R' S) → Algebra R (WithAbs v)