'LatticeGauge.AllFacesBlocking.sq_sum_fin_four_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.AllFacesBlocking.block_energy_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.AllFacesBlocking.fine_energy_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.AllFacesBlocking.equal_split_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.AllFacesBlocking.smooth_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.AllFacesBlocking.quartic_expand' depends on axioms: [propext, Classical.choice, Quot.sound]
