'OrchardMath.Millennium.HardySignParity.sum_even_sign_character_four' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]
'OrchardMath.Millennium.HardySignParityAudit.exact_eight_sign_identity' depends on axioms: [propext,
 Classical.choice,
 Quot.sound]