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