'SizeSplitKP.sum_split_by_card' depends on axioms: [propext, Classical.choice, Quot.sound]
'SizeSplitKP.fat_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SizeSplitKP.geometric_tail_le' depends on axioms: [propext, Classical.choice, Quot.sound]
'SizeSplitKP.size_split_site_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'SizeSplitKP.fat_condition_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'SizeSplitKP.allowed_eps_scale' depends on axioms: [propext, Classical.choice, Quot.sound]
