'EuclideanPath.GapBridge.edge_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.edge_sum'' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.pair_sum_succ' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.geom_shift' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.pair_sum_closed' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.discrete_limit_ge' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.window_ratio_closed' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.window_factor_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.poincare_lower_of_gap' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.local_rayleigh_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.fourier_weight_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.oscillating_ratio_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.gap_lower_of_poincare_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.power_lower_half' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.linear_exponent_does_not_bridge' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.rotor_ratio_unbounded' depends on axioms: [propext, Classical.choice, Quot.sound]
'EuclideanPath.GapBridge.rotor_gap_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
