theorem kl_positivity_for_grothendieck_group (C : CoxeterGroupData) (y w : C.W) (n : ℕ) : 0 ≤ (KazhdanLusztigPoly C y w).coeff n

theorem kl_multiplicity_in_grothendieck_group {R : Type u} [Field R] [IsAlgClosed R] [CharZero R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (C : CoxeterGroupData) (compat : CoxeterWeylCompatibility C rd wg) (lam : ↥Δ.𝔥 →ₗ[R] R) (hlam_dr : IsDominantRegularWeight rd wg lam) (y w : C.W) : ↑(categoryO_multiplicity C rd wg compat lam y w) = Polynomial.eval 1 (KazhdanLusztigPoly C y w)