D (axiom)
DecidableSet.eq_dec [in Coq.Logic.Eqdep_dec]
DecidableSet.U [in Coq.Logic.Eqdep_dec]
DecidableType.eq_dec [in Coq.Logic.Eqdep_dec]
DecidableType.U [in Coq.Logic.Eqdep_dec]
dependent_unique_choice [in Coq.Logic.ClassicalUniqueChoice]
div [in Coq.Numbers.Cyclic.Int63.Int63]
div [in Coq.Floats.PrimFloat]
diveucl [in Coq.Numbers.Cyclic.Int63.Int63]
diveucl_21_spec [in Coq.Numbers.Cyclic.Int63.Int63]
diveucl_def_spec [in Coq.Numbers.Cyclic.Int63.Int63]
diveucl_21 [in Coq.Numbers.Cyclic.Int63.Int63]
DivMod.div [in Coq.Numbers.NatInt.NZDiv]
DivMod.modulo [in Coq.Numbers.NatInt.NZDiv]
div_spec [in Coq.Numbers.Cyclic.Int63.Int63]
div_spec [in Coq.Floats.FloatAxioms]