'AnalyticFloor.small_field_angle_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'AnalyticFloor.floor_necessary' depends on axioms: [propext, Classical.choice, Quot.sound]
'AnalyticFloor.floor_antitone' depends on axioms: [propext, Classical.choice, Quot.sound]
