theorem BNPair.cell_inv_from_bnpair {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (w : M.Group) (g : G) (hg : g ∈ bp.bruhatCell w) : g⁻¹ ∈ bp.bruhatCell w⁻¹

Bruhat cell inversion: $g \in BwB \;\Rightarrow\; g^{-1} \in Bw^{-1}B$, i.e. $C(w)^{-1} = C(w^{-1})$.