'LatticeGauge.QuarticConeNorm.ratio_sandwich' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.QuarticConeNorm.ledger' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.QuarticConeNorm.transfer' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.QuarticConeNorm.cone_b_to_a' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.QuarticConeNorm.stein_floor' depends on axioms: [propext, Classical.choice, Quot.sound]
