noncomputable def BNPair.BruhatProperties.fromAxioms {G : Type u_1} [Group G] {B_idx : Type u_2} [DecidableEq B_idx] [Fintype B_idx] {M : CoxeterMatrix B_idx} (bp : BNPair G M) (ax : BNPairAxioms bp) : bp.BruhatProperties

Assemble the full BruhatProperties bundle (cell cover/disjointness/inversion/multiplication within parabolics, conjugator targeting, finiteness) for a BN-pair from its axioms.