'LatticeGaugeWeightedTailBound.weighted_geom_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeWeightedTailBound.weighted_geom_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeWeightedTailBound.weighted_tail_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeWeightedTailBound.linear_prefactor_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeWeightedTailBound.weighted_sum_uniform_linear' depends on axioms: [propext, Classical.choice, Quot.sound]
