∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O →
    ∀ {p : ℕ} {x : O},
      (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0 →
        ModP.preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) x) = v ((algebraMap O K) x)