'zero_or_succ' does not depend on any axioms
'no_largest' does not depend on any axioms
'add_comm'' does not depend on any axioms
'add_assoc'' does not depend on any axioms
'sum_of_four' depends on axioms: [propext, Quot.sound]
'left_distrib'' does not depend on any axioms
'split_at_ten' depends on axioms: [propext]
'place_value' depends on axioms: [propext]
'place_value_base' depends on axioms: [propext]
'sub_add_cancel_iff' depends on axioms: [propext, Quot.sound]
'subtraction_is_not_inverse' does not depend on any axioms