{R : Type u_1} →
  [inst : Ring R] →
    {Γ₀ : Type u_2} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        {v : Valuation R Γ₀} → (∃ x, v x ≠ 0 ∧ v x ≠ 1) → (hom : Γ₀ →*₀ NNReal) → StrictMono ⇑hom → v.RankOne