theorem BNPair.cell_cover_unconditional {G : Type u_1} [Group G] {B_idx : Type u_2} {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) (g : G) : ∃ (w : M.Group), g ∈ bp.bruhatCell w

Unconditional cell-cover restatement: every $g \in G$ lies in some Bruhat cell $C(w) = BwB$, i.e. $G = \bigcup_{w \in W} BwB$.