'Erdos709.checker_extremalScale_le_fourteen_three_sevenths' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos709.checker_extremalScale_log_katz_bounds' depends on axioms: [propext, Classical.choice, Quot.sound]
'Erdos709.KatzTao.four_projection_card_pow_le' depends on axioms: [propext, Classical.choice, Quot.sound]
