'Kenoma.SerialSpecimenReal.energy_factor' depends on axioms: [propext, Classical.choice, Quot.sound] 'Kenoma.SerialSpecimenReal.energy_nonnegative' depends on axioms: [propext, Classical.choice, Quot.sound] 'Kenoma.SerialSpecimenReal.energy_zero_iff' depends on axioms: [propext, Classical.choice, Quot.sound] 'Kenoma.SerialSpecimenReal.energy_hasDerivAt' depends on axioms: [propext, Classical.choice, Quot.sound] 'Kenoma.SerialSpecimenReal.nominal_factor_and_cauchy' depends on axioms: [propext, Classical.choice, Quot.sound] 'Kenoma.SerialSpecimenReal.nominal_sign' depends on axioms: [propext, Classical.choice, Quot.sound] 'Kenoma.SerialSpecimenReal.nominal_difference' depends on axioms: [propext, Classical.choice, Quot.sound] 'Kenoma.SerialSpecimenReal.nominal_strictMono' depends on axioms: [propext, Classical.choice, Quot.sound] 'Kenoma.SerialSpecimenReal.homogeneous_root_unique' depends on axioms: [propext, Classical.choice, Quot.sound] 'Kenoma.SerialSpecimenReal.area_length_volume' depends on axioms: [propext, Classical.choice, Quot.sound] 'Kenoma.SerialSpecimenReal.same_force_tension_order' depends on axioms: [propext, Classical.choice, Quot.sound] 'Kenoma.SerialSpecimenReal.same_force_compression_order' depends on axioms: [propext, Classical.choice, Quot.sound]