def IsDominantCorootNonneg {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) [LinearOrder R] [IsStrictOrderedRing R] (lam : ↥Δ.𝔥 →ₗ[R] R) : Prop

theorem normSq_diff_factorization {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) (B : WeightBilinForm wg) (lam phi alpha : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) (halpha_pos : alpha ∈ rd.posRoots) (hpair : rd.corootPairing phi alpha = ↑n) : B.normSq (lam - phi + n • alpha) - B.normSq (lam - phi) = ↑n * rd.corootPairing lam alpha * B.form alpha alpha

theorem form_posRoot_pos_of_WeightBilinForm {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (B : WeightBilinForm wg) (alpha : ↥Δ.𝔥 →ₗ[R] R) (halpha_pos : alpha ∈ rd.posRoots) : 0 < B.form alpha alpha

theorem normSq_le_of_single_step {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (B : WeightBilinForm wg) (lam a b : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantCorootNonneg rd lam) (hstep : ∃ (α : ↥Δ.𝔥 →ₗ[R] R), ReflectionLT rd α a b) : B.normSq (lam - b) ≤ B.normSq (lam - a)

theorem corootPairing_lam_eq_zero_of_normSq_eq {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (B : WeightBilinForm wg) (lam b alpha : ↥Δ.𝔥 →ₗ[R] R) (n : ℕ) (halpha_pos : alpha ∈ rd.posRoots) (hn_pos : 0 < n) (hpair : rd.corootPairing b alpha = ↑n) (h_eq : B.normSq (lam - b) = B.normSq (lam - b + n • alpha)) : rd.corootPairing lam alpha = 0

theorem weylStab_of_normSq_eq_single_step {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (rs : RootSystemWithReflections rd wg) (B : WeightBilinForm wg) (lam a b : ↥Δ.𝔥 →ₗ[R] R) (_hlam_dom : IsDominantCorootNonneg rd lam) (hstep : ∃ (α : ↥Δ.𝔥 →ₗ[R] R), ReflectionLT rd α a b) (h_eq : B.normSq (lam - b) = B.normSq (lam - a)) : ∃ w ∈ WeylStabilizer rd wg lam, wg.dualAction w b = a

theorem normSq_le_of_bruhatLE {R : Type u} [CommRing R] {𝔤 : Type u} [LieRing 𝔤] [LieAlgebra R 𝔤] {Δ : TriangularDecomposition R 𝔤} (rd : PositiveRootData Δ) (wg : WeylGroupData Δ) [LinearOrder R] [IsStrictOrderedRing R] (B : WeightBilinForm wg) (lam phi psi : ↥Δ.𝔥 →ₗ[R] R) (hlam_dom : IsDominantCorootNonneg rd lam) (hBruhat : BruhatLE rd psi phi) : B.normSq (lam - phi) ≤ B.normSq (lam - psi)