∀ {R : Type u_5} [inst : Semiring R] [inst_1 : DecidablePred fun x => x = 0] [inst_2 : NoZeroDivisors R] {S : Type u_6}
  [inst_3 : Semiring S] [inst_4 : PartialOrder S] [inst_5 : IsOrderedRing S] [inst_6 : Nontrivial S],
  AbsoluteValue.trivial =
    { toFun := fun x => if x = 0 then 0 else 1, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }