theorem CoxeterSystem.mem_alternatingWord {B : Type u_1} [DecidableEq B] (i j : B) (m : ℕ) (b : B) (hb : b ∈ alternatingWord i j m) : b = i ∨ b = j

Every letter of an alternating word $iji j \cdots$ of length $m$ equals either $i$ or $j$.

theorem CoxeterSystem.parabolic_decomp_rank2 {B : Type u_1} [DecidableEq B] {W : Type u_2} [Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (s t : B) (hst : s ≠ t) : ∃ (x : W) (y_word : List B), x * cs.wordProd y_word = w ∧ cs.length (x * cs.simple s) = cs.length x + 1 ∧ cs.length (x * cs.simple t) = cs.length x + 1 ∧ (∀ b ∈ y_word, b = s ∨ b = t) ∧ cs.length x + y_word.length = cs.length w

Rank-2 parabolic decomposition: for every $w \in W$ and distinct $s, t \in S$, there exist $x \in W$ and a word $y$ on the alphabet $\{s, t\}$ such that $w = x \cdot y$, $\ell(x \cdot s) = \ell(x \cdot t) = \ell(x) + 1$, and lengths add: $\ell(x) + \mathrm{len}(y) = \ell(w)$.