'ClassStepRemainder.bounded_orbit_small' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.norm_step_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.orbit_in_small_ball' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.coupling_remainder_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassStepRemainder.small_rem_form' depends on axioms: [propext, Classical.choice, Quot.sound]
