'ClassSiteSum.site_sum_le_class_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassSiteSum.hsite_of_class_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassSiteSum.single_class_sum' depends on axioms: [propext, Classical.choice, Quot.sound]
'ClassSiteSum.tail_le_of_ratio' depends on axioms: [propext, Classical.choice, Quot.sound]
