theorem CoxeterBruhat.bruhat_chain_property_unconditional {B : Type u_1} [DecidableEq B] [Fintype B] (M : CoxeterMatrix B) (hSEC_full : StrongExchangeCondition M.toCoxeterSystem) (hRSP : ReducedSublistProperty M.toCoxeterSystem) {v w : M.Group} (hvw : BruhatLT M.toCoxeterSystem v w) : ∃ (n : ℕ) (f : Fin (n + 2) → M.Group), f ⟨0, ⋯⟩ = v ∧ f ⟨n + 1, ⋯⟩ = w ∧ ∀ (i : Fin (n + 1)), BruhatLT M.toCoxeterSystem (f ⟨↑i, ⋯⟩) (f ⟨↑i + 1, ⋯⟩) ∧ M.toCoxeterSystem.length (f ⟨↑i, ⋯⟩) + 1 = M.toCoxeterSystem.length (f ⟨↑i + 1, ⋯⟩)

Chain property for the Bruhat order: assuming the Strong Exchange Condition and the Reduced Sublist Property, any strict Bruhat inequality $v < w$ can be refined to a chain $v = u_0 < u_1 < \cdots < u_{n+1} = w$ in which consecutive elements differ by exactly one in length.