'LatticeGaugeRatioTwoCriterion.kappa_a_of_ibp' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeRatioTwoCriterion.kappa_ab_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeRatioTwoCriterion.ratio_two_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeRatioTwoCriterion.ratio_eq_two_add' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeRatioTwoCriterion.one_loop_D' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeRatioTwoCriterion.one_loop_D_u1' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeRatioTwoCriterion.gamma_family_one_loop_lower' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeRatioTwoCriterion.fund_adj_one_loop_root' depends on axioms: [propext, Classical.choice, Quot.sound]
'LatticeGaugeRatioTwoCriterion.no_pointwise_sqrt_one_loop' depends on axioms: [propext, Classical.choice, Quot.sound]
