'FaceSpectrum.smul_log_le_log' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.neg_log_le_chord' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.sum_neg_log_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.logMoment_le_per_face' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.chord_slope_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.single_face_case' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.chernoff_glue' depends on axioms: [propext, Classical.choice, Quot.sound]
'FaceSpectrum.tilt_range' depends on axioms: [propext, Classical.choice, Quot.sound]
