∀ {K : Type u_2} {Γ : Type u_1} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} {a b : Polynomial K},
  v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0 → a ∉ {p | v ↑p < 1 ∧ p ≠ 0} → 1 ≤ v ↑a