'LatticeGauge.DoubleWellTestbed.ratioR_free_eq_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.DoubleWellTestbed.ratioR_x_normalisation' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.DoubleWellTestbed.inv_le_div_sq_of_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.DoubleWellTestbed.resolvent_le_form_div_sq' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.DoubleWellTestbed.local_rayleigh_ratio_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.DoubleWellTestbed.local_rayleigh_attained' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGauge.DoubleWellTestbed.power_level_log_ratio_tendsto_zero' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
