theorem CellDisjoint.bruhatCell_mul_B_left {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {w : M.Group} {g b : G} (hg : g ∈ bp.bruhatCell w) (hb : b ∈ bp.B) : b * g ∈ bp.bruhatCell w

Left $B$-absorption: $B \cdot C(w) \subseteq C(w)$.

theorem CellDisjoint.bruhatCell_mul_B_right {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) {w : M.Group} {g b : G} (hg : g ∈ bp.bruhatCell w) (hb : b ∈ bp.B) : g * b ∈ bp.bruhatCell w

Right $B$-absorption: $C(w) \cdot B \subseteq C(w)$.

theorem CellDisjoint.N_lift_mem_bruhatCell_simple {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (n : ↥bp.N) (s : B_idx) (hn : bp.π n = M.toCoxeterSystem.simple s) : ↑n ∈ bp.bruhatCell (M.toCoxeterSystem.simple s)

A lift $n \in N$ of a simple reflection $s$ lies in the cell $C(s) = BsB$.