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

'PaperToLean.Steffensen.divided_difference' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.raw_equivalence' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.fixed_root' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.exact_error' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.safe_denominator' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.bracket' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Steffensen.quadratic_bound' depends on axioms: [propext, Classical.choice, Quot.sound]