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

'PaperToLean.Jury.real_root_upper' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Jury.real_root_inside' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Jury.root_parts' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Jury.nonreal_modulus' depends on axioms: [propext, Classical.choice, Quot.sound]
'PaperToLean.Jury.quadratic_sufficient' depends on axioms: [propext, Classical.choice, Quot.sound]