'BioSwarmCheck.C_jumps' depends on axioms: [propext, Classical.choice, Quot.sound] 'BioSwarmCheck.U_norm' depends on axioms: [propext, Classical.choice, Quot.sound] 'BioSwarmCheck.four_fixed_points' depends on axioms: [propext, Classical.choice, Quot.sound]