'Book12.addc_correct' depends on axioms: [propext, Quot.sound]
'Book12.carry_small' depends on axioms: [propext, Quot.sound]
'Book12.written_is_digit' does not depend on any axioms
'Book12.quot_rem_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book12.quot_rem_exist' depends on axioms: [propext]
'Book12.rem_step' depends on axioms: [propext]
'Book12.remH_gen' depends on axioms: [propext]
'Book12.remH_correct' depends on axioms: [propext]
'Book12.nines' depends on axioms: [propext, Quot.sound]
'Book12.addc_correct' depends on axioms: [propext, Quot.sound]
'Book12.carry_small' depends on axioms: [propext, Quot.sound]
'Book12.written_is_digit' does not depend on any axioms
'Book12.quot_rem_unique' depends on axioms: [propext, Classical.choice, Quot.sound]
'Book12.quot_rem_exist' depends on axioms: [propext]
'Book12.rem_step' depends on axioms: [propext]
'Book12.remH_gen' depends on axioms: [propext]
'Book12.remH_correct' depends on axioms: [propext]
'Book12.nines' depends on axioms: [propext, Quot.sound]