Lean (version 4.7.0, commit v4.7.0, Release)
exitCode=0
'HunterAuthored.finite_fixed_point_clamp_bounds' depends on axioms: [Classical.choice, propext, Quot.sound]