Lean 4.33.1
Dependencies: Mathlib 4.33.1 (see bundled lake-manifest.json)
File: Halley.lean
SHA-256: c51faf612bca380035e0049661ec13da9bf3ced2d8f0371678c78c7456e3dfcc
Result: passed

'PaperToLean.Halley.denominator_pos' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.positive_step' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.cubic_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.cubic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.ratio_cubed' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.iterate_positive' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Halley.ratio_at_every_step' depends on axioms: [propext, Classical.choice, Quot.sound]