Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(68863 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(985 entries)

Binder Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(44709 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(761 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1497 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(570 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(11380 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(976 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(603 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(298 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(460 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(476 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(811 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1157 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4018 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(162 entries)

---

D

D [constructor, in Coq.micromega.Tauto]
Da [constructor, in Coq.Init.Hexadecimal]
Dadd [lemma, in Coq.Reals.Rderiv]
Datan_eq_DatanSeq_interv [lemma, in Coq.Reals.Ratan]
Datan_continuity [lemma, in Coq.Reals.Ratan]
Datan_is_datan [lemma, in Coq.Reals.Ratan]
Datan_CVU_prelim [lemma, in Coq.Reals.Ratan]
Datan_lim [lemma, in Coq.Reals.Ratan]
Datan_seq_CV_0 [lemma, in Coq.Reals.Ratan]
Datan_seq_decreasing [lemma, in Coq.Reals.Ratan]
Datan_seq_increasing [lemma, in Coq.Reals.Ratan]
Datan_sum_eq [lemma, in Coq.Reals.Ratan]
Datan_seq_pos [lemma, in Coq.Reals.Ratan]
Datan_seq_Rabs [lemma, in Coq.Reals.Ratan]
Datan_seq [definition, in Coq.Reals.Ratan]
Datatypes [library]
Db [constructor, in Coq.Init.Hexadecimal]
Dc [constructor, in Coq.Init.Hexadecimal]
Dcomp [lemma, in Coq.Reals.Rderiv]
Dcompare [lemma, in Coq.PArith.BinPos]
Dcompare_inf [lemma, in Coq.ZArith.ZArith_dec]
Dconst [lemma, in Coq.Reals.Rderiv]
DC:20 [binder, in Coq.micromega.DeclConstant]
DC:9 [binder, in Coq.micromega.DeclConstant]
Dd [constructor, in Coq.Init.Hexadecimal]
DDcut_limit [lemma, in Coq.Reals.Abstract.ConstructiveLUB]
DDcut_limit_fix [definition, in Coq.Reals.Abstract.ConstructiveLUB]
DDdec [projection, in Coq.Reals.Abstract.ConstructiveLUB]
DDhigh [projection, in Coq.Reals.Abstract.ConstructiveLUB]
DDhighProp [projection, in Coq.Reals.Abstract.ConstructiveLUB]
DDinterval [projection, in Coq.Reals.Abstract.ConstructiveLUB]
DDlow [projection, in Coq.Reals.Abstract.ConstructiveLUB]
DDlowProp [projection, in Coq.Reals.Abstract.ConstructiveLUB]
DDlow_below_up [lemma, in Coq.Reals.Abstract.ConstructiveLUB]
DDproper [projection, in Coq.Reals.Abstract.ConstructiveLUB]
DDupcut [projection, in Coq.Reals.Abstract.ConstructiveLUB]
De [constructor, in Coq.Init.Hexadecimal]
Dec [constructor, in Coq.Init.Numeral]
dec [abbreviation, in Coq.Program.Utils]
DecBool [library]
decidability [section, in Coq.ZArith.ZArith_dec]
decidability.x [variable, in Coq.ZArith.ZArith_dec]
decidability.y [variable, in Coq.ZArith.ZArith_dec]
decidable [definition, in Coq.Logic.Decidable]
decidable [definition, in Coq.ssr.ssrbool]
Decidable [record, in Coq.Classes.DecidableClass]
Decidable [library]
DecidableClass [library]
DecidableEqDep [module, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet [module, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.eq_dep_eq [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.eq_rect_eq [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.inj_pairT2 [abbreviation, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.inj_pair2 [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.inj_pairP2 [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.N [module, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.Streicher_K [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.UIP [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDepSet.UIP_refl [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.eq_dep_eq [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.eq_rect_eq [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.inj_pairP2 [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.inj_pairT2 [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.Streicher_K [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.UIP [lemma, in Coq.Logic.Eqdep_dec]
DecidableEqDep.UIP_refl [lemma, in Coq.Logic.Eqdep_dec]
DecidableEquivalence [record, in Coq.Classes.EquivDec]
DecidableEquivalence [inductive, in Coq.Classes.EquivDec]
DecidableSet [module, in Coq.Logic.Eqdep_dec]
DecidableSetoid [record, in Coq.Classes.SetoidDec]
DecidableSetoid [inductive, in Coq.Classes.SetoidDec]
DecidableSet.eq_dec [axiom, in Coq.Logic.Eqdep_dec]
DecidableSet.U [axiom, in Coq.Logic.Eqdep_dec]
DecidableType [module, in Coq.Logic.Eqdep_dec]
DecidableType [module, in Coq.Structures.DecidableType]
DecidableType [module, in Coq.Structures.Equalities]
DecidableType [library]
DecidableTypeBoth [module, in Coq.Structures.Equalities]
DecidableTypeBoth' [module, in Coq.Structures.Equalities]
DecidableTypeEx [library]
DecidableTypeFull [module, in Coq.Structures.Equalities]
DecidableTypeFull' [module, in Coq.Structures.Equalities]
DecidableTypeOrig [module, in Coq.Structures.Equalities]
DecidableTypeOrig' [module, in Coq.Structures.Equalities]
DecidableType' [module, in Coq.Structures.Equalities]
DecidableType.eq_dec [axiom, in Coq.Logic.Eqdep_dec]
DecidableType.U [axiom, in Coq.Logic.Eqdep_dec]
Decidable_valid [instance, in Coq.btauto.Algebra]
Decidable_null [instance, in Coq.btauto.Algebra]
Decidable_eq_poly [instance, in Coq.btauto.Algebra]
Decidable_PosLe [instance, in Coq.btauto.Algebra]
Decidable_PosLt [instance, in Coq.btauto.Algebra]
Decidable_PosEq [instance, in Coq.btauto.Algebra]
Decidable_complete_alt [lemma, in Coq.btauto.Algebra]
Decidable_sound_alt [lemma, in Coq.btauto.Algebra]
Decidable_complete [lemma, in Coq.btauto.Algebra]
Decidable_sound [lemma, in Coq.btauto.Algebra]
decidable_eq [definition, in Coq.Lists.ListDec]
Decidable_eq_Z [instance, in Coq.Classes.DecidableClass]
Decidable_le_nat [instance, in Coq.Classes.DecidableClass]
Decidable_eq_nat [instance, in Coq.Classes.DecidableClass]
Decidable_eq_bool [instance, in Coq.Classes.DecidableClass]
Decidable_complete_alt [lemma, in Coq.Classes.DecidableClass]
Decidable_sound_alt [lemma, in Coq.Classes.DecidableClass]
Decidable_complete [lemma, in Coq.Classes.DecidableClass]
Decidable_sound [lemma, in Coq.Classes.DecidableClass]
Decidable_spec [projection, in Coq.Classes.DecidableClass]
Decidable_witness [projection, in Coq.Classes.DecidableClass]
Decide [module, in Coq.FSets.FSetDecide]
Decide [module, in Coq.MSets.MSetDecide]
decide [definition, in Coq.Classes.DecidableClass]
decide [lemma, in Coq.Logic.Diaconescu]
decide_right [lemma, in Coq.Init.Tactics]
decide_left [lemma, in Coq.Init.Tactics]
decide:4 [binder, in Coq.Init.Tactics]
decide:8 [binder, in Coq.Init.Tactics]
Decimal [constructor, in Coq.Init.Decimal]
decimal [inductive, in Coq.Init.Decimal]
Decimal [library]
DecimalExp [constructor, in Coq.Init.Decimal]
DecimalFacts [library]
DecimalN [library]
DecimalNat [library]
DecimalPos [library]
DecimalQ [library]
DecimalString [library]
DecimalZ [library]
decimal_exp [definition, in Coq.Reals.Rfunctions]
decimal_dot:30 [binder, in Coq.QArith.QArith_base]
decimal_exponent:20 [binder, in Coq.QArith.QArith_base]
DeclaredConstant [record, in Coq.micromega.DeclConstant]
DeclarePredSortOfSimpl [module, in Coq.ssr.ssrbool]
DeclConstant [library]
decomp_sum [lemma, in Coq.Reals.PartSum]
decomp_sum [lemma, in Coq.Reals.Abstract.ConstructiveSum]
decP [definition, in Coq.ssr.ssrbool]
decPcases [lemma, in Coq.ssr.ssrbool]
decQ:78 [binder, in Coq.ssr.ssrbool]
decrease_seq_transit [lemma, in Coq.Reals.Runcountable]
decreasing [definition, in Coq.Reals.Ranalysis1]
decreasing_prop [lemma, in Coq.Reals.SeqProp]
decreasing_ineq [lemma, in Coq.Reals.SeqProp]
decreasing_cv [lemma, in Coq.Reals.SeqProp]
decreasing_growing [lemma, in Coq.Reals.SeqProp]
DecStrOrder [module, in Coq.Structures.Orders]
DecStrOrder' [module, in Coq.Structures.Orders]
dec_functional_relation [lemma, in Coq.Logic.Decidable]
dec_iff [lemma, in Coq.Logic.Decidable]
dec_imp [lemma, in Coq.Logic.Decidable]
dec_not [lemma, in Coq.Logic.Decidable]
dec_and [lemma, in Coq.Logic.Decidable]
dec_or [lemma, in Coq.Logic.Decidable]
dec_False [lemma, in Coq.Logic.Decidable]
dec_True [lemma, in Coq.Logic.Decidable]
dec_not_not [lemma, in Coq.Logic.Decidable]
dec_ge [lemma, in Coq.Arith.Compare_dec]
dec_gt [lemma, in Coq.Arith.Compare_dec]
dec_lt [lemma, in Coq.Arith.Compare_dec]
dec_le [lemma, in Coq.Arith.Compare_dec]
dec_inh_nat_subset_has_unique_least_element [lemma, in Coq.Arith.Wf_nat]
Dec_in_Type.dec [variable, in Coq.Lists.ListDec]
Dec_in_Type.A [variable, in Coq.Lists.ListDec]
Dec_in_Type [section, in Coq.Lists.ListDec]
Dec_in_Prop.dec [variable, in Coq.Lists.ListDec]
Dec_in_Prop.A [variable, in Coq.Lists.ListDec]
Dec_in_Prop [section, in Coq.Lists.ListDec]
dec_Zge [lemma, in Coq.ZArith.Zorder]
dec_Zgt [lemma, in Coq.ZArith.Zorder]
dec_Zne [lemma, in Coq.ZArith.Zorder]
dec_Zlt [abbreviation, in Coq.ZArith.Zorder]
dec_Zle [abbreviation, in Coq.ZArith.Zorder]
dec_eq [abbreviation, in Coq.ZArith.Zorder]
dec_eq_nat [lemma, in Coq.Arith.Peano_dec]
Dec2Bool [module, in Coq.Structures.Equalities]
DedekindDecCut [record, in Coq.Reals.Abstract.ConstructiveLUB]
DefaultKeying [module, in Coq.ssr.ssrbool]
DefaultKeying.default_keyed_qualifier [definition, in Coq.ssr.ssrbool]
DefaultKeying.default_keyed_pred [definition, in Coq.ssr.ssrbool]
DefaultPredKey [constructor, in Coq.ssr.ssrbool]
DefaultRelation [record, in Coq.Classes.SetoidTactics]
default_relation [definition, in Coq.Classes.SetoidTactics]
default_isIn_ok [lemma, in Coq.setoid_ring.Field_theory]
default_isIn [definition, in Coq.setoid_ring.Field_theory]
default:104 [binder, in Coq.Lists.List]
default:110 [binder, in Coq.Lists.List]
default:126 [binder, in Coq.Lists.List]
default:2 [binder, in Coq.Lists.List]
Definitions [section, in Coq.btauto.Algebra]
DEFINITIONS [section, in Coq.micromega.OrderedRing]
DEFINITIONS [section, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM [section, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.C [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.cadd [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.ceqb [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.cI [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.cmul [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.cO [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.copp [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.csub [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.DIV [section, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.DIV.cdiv [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.phi [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.SIGN [section, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.MORPHISM.SIGN.get_sign [variable, in Coq.setoid_ring.Ring_theory]
_ ?=! _ [notation, in Coq.setoid_ring.Ring_theory]
_ *! _ [notation, in Coq.setoid_ring.Ring_theory]
_ -! _ [notation, in Coq.setoid_ring.Ring_theory]
_ +! _ [notation, in Coq.setoid_ring.Ring_theory]
-! _ [notation, in Coq.setoid_ring.Ring_theory]
[ _ ] [notation, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.morph_req [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.POWER [section, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.POWER.Cpow [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.POWER.Cp_phi [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.POWER.rpow [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.R [variable, in Coq.micromega.OrderedRing]
DEFINITIONS.R [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.radd [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.req [variable, in Coq.micromega.OrderedRing]
DEFINITIONS.req [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.reqb [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.rI [variable, in Coq.micromega.OrderedRing]
DEFINITIONS.rI [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.rle [variable, in Coq.micromega.OrderedRing]
DEFINITIONS.rlt [variable, in Coq.micromega.OrderedRing]
DEFINITIONS.rminus [variable, in Coq.micromega.OrderedRing]
DEFINITIONS.rmul [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.rO [variable, in Coq.micromega.OrderedRing]
DEFINITIONS.rO [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.ropp [variable, in Coq.micromega.OrderedRing]
DEFINITIONS.ropp [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.rplus [variable, in Coq.micromega.OrderedRing]
DEFINITIONS.Rsth [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.rsub [variable, in Coq.setoid_ring.Ring_theory]
DEFINITIONS.rtimes [variable, in Coq.micromega.OrderedRing]
_ < _ [notation, in Coq.micromega.OrderedRing]
_ <= _ [notation, in Coq.micromega.OrderedRing]
_ ~= _ [notation, in Coq.micromega.OrderedRing]
_ == _ [notation, in Coq.micromega.OrderedRing]
_ - _ [notation, in Coq.micromega.OrderedRing]
_ * _ [notation, in Coq.micromega.OrderedRing]
_ + _ [notation, in Coq.micromega.OrderedRing]
_ - _ [notation, in Coq.setoid_ring.Ring_theory]
_ * _ [notation, in Coq.setoid_ring.Ring_theory]
_ + _ [notation, in Coq.setoid_ring.Ring_theory]
_ == _ [notation, in Coq.setoid_ring.Ring_theory]
- _ [notation, in Coq.micromega.OrderedRing]
- _ [notation, in Coq.setoid_ring.Ring_theory]
0 [notation, in Coq.micromega.OrderedRing]
0 [notation, in Coq.setoid_ring.Ring_theory]
1 [notation, in Coq.micromega.OrderedRing]
1 [notation, in Coq.setoid_ring.Ring_theory]
definition_of_noetherian [constructor, in Coq.Sets.Relations_3]
Definition_of_chain [constructor, in Coq.Sets.Cpo]
Definition_of_cpo [constructor, in Coq.Sets.Cpo]
Definition_of_Conditionally_complete [constructor, in Coq.Sets.Cpo]
Definition_of_Complete [constructor, in Coq.Sets.Cpo]
Definition_of_Directed [constructor, in Coq.Sets.Cpo]
Definition_of_covers [constructor, in Coq.Sets.Partial_Order]
Definition_of_PO [constructor, in Coq.Sets.Partial_Order]
Definition_of_PER [constructor, in Coq.Sets.Relations_1]
Definition_of_equivalence [constructor, in Coq.Sets.Relations_1]
Definition_of_order [constructor, in Coq.Sets.Relations_1]
Definition_of_preorder [constructor, in Coq.Sets.Relations_1]
Definition_of_Power_set [constructor, in Coq.Sets.Powerset]
Defn_of_Approximant [constructor, in Coq.Sets.Infinite_sets]
Defs [section, in Coq.Classes.RelationClasses]
Defs [section, in Coq.ssr.ssrclasses]
defs [section, in Coq.Sorting.Sorted]
defs [section, in Coq.Sets.Uniset]
Defs [section, in Coq.Classes.CRelationClasses]
defs [section, in Coq.Sorting.Heap]
defs.A [variable, in Coq.Sorting.Sorted]
defs.A [variable, in Coq.Sets.Uniset]
defs.A [variable, in Coq.Sorting.Heap]
Defs.complement [section, in Coq.Classes.RelationClasses]
Defs.complement [section, in Coq.Classes.CRelationClasses]
defs.emptyBag [variable, in Coq.Sorting.Heap]
defs.eqA [variable, in Coq.Sets.Uniset]
defs.eqA [variable, in Coq.Sorting.Heap]
defs.eqA_dec [variable, in Coq.Sets.Uniset]
defs.eqA_dec [variable, in Coq.Sorting.Heap]
Defs.flip [section, in Coq.Classes.RelationClasses]
Defs.flip [section, in Coq.Classes.CRelationClasses]
defs.gtA [variable, in Coq.Sorting.Heap]
defs.leA [variable, in Coq.Sorting.Heap]
defs.leA_antisym [variable, in Coq.Sorting.Heap]
defs.leA_trans [variable, in Coq.Sorting.Heap]
defs.leA_refl [variable, in Coq.Sorting.Heap]
defs.leA_dec [variable, in Coq.Sorting.Heap]
Defs.Leibniz [section, in Coq.Classes.RelationClasses]
Defs.Leibniz [section, in Coq.Classes.CRelationClasses]
defs.R [variable, in Coq.Sorting.Sorted]
defs.singletonBag [variable, in Coq.Sorting.Heap]
def:30 [binder, in Coq.Logic.Eqdep_dec]
def:30 [binder, in Coq.btauto.Reflect]
def:44 [binder, in Coq.btauto.Reflect]
def:48 [binder, in Coq.btauto.Algebra]
def:49 [binder, in Coq.btauto.Reflect]
def:5 [binder, in Coq.funind.Recdef]
DEF:50 [binder, in Coq.micromega.RMicromega]
def:54 [binder, in Coq.btauto.Reflect]
def:59 [binder, in Coq.btauto.Reflect]
def:63 [binder, in Coq.btauto.Reflect]
deg_rad [lemma, in Coq.Reals.Rtrigo_calc]
deletion [lemma, in Coq.Program.Equality]
Delta [definition, in Coq.Reals.R_sqrt]
delta [definition, in Coq.Logic.ExtensionalityFacts]
Delta [record, in Coq.Logic.ExtensionalityFacts]
Delta_is_pos [definition, in Coq.Reals.R_sqrt]
delta:115 [binder, in Coq.Reals.Ranalysis1]
delta:116 [binder, in Coq.Reals.RiemannInt]
delta:138 [binder, in Coq.Reals.RiemannInt]
delta:268 [binder, in Coq.Reals.Ranalysis5]
delta:271 [binder, in Coq.Reals.Ranalysis5]
delta:30 [binder, in Coq.rtauto.Bintree]
delta:384 [binder, in Coq.Reals.Rtopology]
delta:44 [binder, in Coq.Reals.Rtopology]
delta:46 [binder, in Coq.Reals.Rtopology]
delta:5 [binder, in Coq.Reals.Rtopology]
delta:9 [binder, in Coq.Reals.Rtopology]
del_tail_int [definition, in Coq.Init.Decimal]
del_tail [definition, in Coq.Init.Decimal]
del_head_int [definition, in Coq.Init.Decimal]
del_head [definition, in Coq.Init.Decimal]
del_tail_nonnil [lemma, in Coq.Numbers.DecimalFacts]
del_head_nonnil [lemma, in Coq.Numbers.DecimalFacts]
del_head_nth [lemma, in Coq.Numbers.DecimalFacts]
del_head_nb_digits [lemma, in Coq.Numbers.DecimalFacts]
del:100 [binder, in Coq.Reals.RiemannInt]
del:105 [binder, in Coq.Reals.RiemannInt]
del:110 [binder, in Coq.Reals.RiemannInt]
del:144 [binder, in Coq.Reals.RiemannInt]
del:148 [binder, in Coq.Reals.RiemannInt]
del:152 [binder, in Coq.Reals.RiemannInt]
del:155 [binder, in Coq.Reals.RiemannInt]
del:159 [binder, in Coq.Reals.RiemannInt]
del:163 [binder, in Coq.Reals.RiemannInt]
del:167 [binder, in Coq.Reals.RiemannInt]
del:171 [binder, in Coq.Reals.RiemannInt]
del:176 [binder, in Coq.Reals.RiemannInt]
del:180 [binder, in Coq.Reals.RiemannInt]
del:185 [binder, in Coq.Reals.RiemannInt]
del:413 [binder, in Coq.Reals.Rtopology]
del:419 [binder, in Coq.Reals.Rtopology]
del:440 [binder, in Coq.Reals.Rtopology]
del:444 [binder, in Coq.Reals.Rtopology]
del:448 [binder, in Coq.Reals.Rtopology]
del:452 [binder, in Coq.Reals.Rtopology]
del:62 [binder, in Coq.Reals.Rtopology]
del:91 [binder, in Coq.Reals.RiemannInt]
del:97 [binder, in Coq.Reals.PSeries_reg]
del:99 [binder, in Coq.Reals.PSeries_reg]
demorgan_inductively_barred_at [definition, in Coq.Logic.WKL]
demorgan_or [definition, in Coq.Logic.WKL]
demorgan1 [abbreviation, in Coq.Bool.Bool]
demorgan2 [abbreviation, in Coq.Bool.Bool]
demorgan3 [abbreviation, in Coq.Bool.Bool]
demorgan4 [abbreviation, in Coq.Bool.Bool]
denorm [definition, in Coq.micromega.RingMicromega]
denorm_correct [lemma, in Coq.micromega.RingMicromega]
denum [projection, in Coq.setoid_ring.Field_theory]
den:301 [binder, in Coq.setoid_ring.Field_theory]
den:306 [binder, in Coq.setoid_ring.Field_theory]
den:32 [binder, in Coq.QArith.QArith_base]
den:337 [binder, in Coq.setoid_ring.Field_theory]
den:346 [binder, in Coq.setoid_ring.Field_theory]
den:350 [binder, in Coq.setoid_ring.Field_theory]
den:359 [binder, in Coq.setoid_ring.Field_theory]
den:370 [binder, in Coq.setoid_ring.Field_theory]
den:46 [binder, in Coq.QArith.QArith_base]
depair [definition, in Coq.Vectors.Fin]
depair_sanity [lemma, in Coq.Vectors.Fin]
DependentEliminationPackage [record, in Coq.Program.Equality]
DependentFunctionalChoice [abbreviation, in Coq.Logic.ChoiceFacts]
DependentFunctionalChoice_on [definition, in Coq.Logic.ChoiceFacts]
DependentFunctionalRelReification [abbreviation, in Coq.Logic.ChoiceFacts]
DependentFunctionalRelReification_on [definition, in Coq.Logic.ChoiceFacts]
DependentMemoFunction [section, in Coq.Lists.StreamMemo]
DependentMemoFunction.A [variable, in Coq.Lists.StreamMemo]
DependentMemoFunction.f [variable, in Coq.Lists.StreamMemo]
DependentMemoFunction.g [variable, in Coq.Lists.StreamMemo]
DependentMemoFunction.Hg_correct [variable, in Coq.Lists.StreamMemo]
DependentMemoFunction.mf [variable, in Coq.Lists.StreamMemo]
DependentMemoFunction.mg [variable, in Coq.Lists.StreamMemo]
dependentReturnType [definition, in Coq.ssr.ssreflect]
Dependent_Equality.P [variable, in Coq.Logic.EqdepFacts]
Dependent_Equality.U [variable, in Coq.Logic.EqdepFacts]
Dependent_Equality [section, in Coq.Logic.EqdepFacts]
dependent_choice [lemma, in Coq.Init.Specif]
Dependent_choice_lemmas.R [variable, in Coq.Init.Specif]
Dependent_choice_lemmas.X [variable, in Coq.Init.Specif]
Dependent_choice_lemmas [section, in Coq.Init.Specif]
dependent_unique_choice [axiom, in Coq.Logic.ClassicalUniqueChoice]
dependent_description [definition, in Coq.Logic.ClassicalDescription]
dependent_unique_choice [lemma, in Coq.Logic.ClassicalDescription]
DepOfNodep [module, in Coq.FSets.FSetBridge]
DepOfNodep.add [definition, in Coq.FSets.FSetBridge]
DepOfNodep.Add [definition, in Coq.FSets.FSetBridge]
DepOfNodep.cardinal [definition, in Coq.FSets.FSetBridge]
DepOfNodep.choose [definition, in Coq.FSets.FSetBridge]
DepOfNodep.choose_equal [lemma, in Coq.FSets.FSetBridge]
DepOfNodep.choose_ok2 [lemma, in Coq.FSets.FSetBridge]
DepOfNodep.choose_ok1 [lemma, in Coq.FSets.FSetBridge]
DepOfNodep.choose_aux [definition, in Coq.FSets.FSetBridge]
DepOfNodep.compare [definition, in Coq.FSets.FSetBridge]
DepOfNodep.compat_P_aux [lemma, in Coq.FSets.FSetBridge]
DepOfNodep.diff [definition, in Coq.FSets.FSetBridge]
DepOfNodep.E [module, in Coq.FSets.FSetBridge]
DepOfNodep.elements [definition, in Coq.FSets.FSetBridge]
DepOfNodep.elt [definition, in Coq.FSets.FSetBridge]
DepOfNodep.Empty [definition, in Coq.FSets.FSetBridge]
DepOfNodep.empty [definition, in Coq.FSets.FSetBridge]
DepOfNodep.eq [definition, in Coq.FSets.FSetBridge]
DepOfNodep.Equal [definition, in Coq.FSets.FSetBridge]
DepOfNodep.equal [definition, in Coq.FSets.FSetBridge]
DepOfNodep.eq_trans [definition, in Coq.FSets.FSetBridge]
DepOfNodep.eq_sym [definition, in Coq.FSets.FSetBridge]
DepOfNodep.eq_refl [definition, in Coq.FSets.FSetBridge]
DepOfNodep.eq_In [definition, in Coq.FSets.FSetBridge]
DepOfNodep.Exists [definition, in Coq.FSets.FSetBridge]
DepOfNodep.exists_ [definition, in Coq.FSets.FSetBridge]
DepOfNodep.fdec [definition, in Coq.FSets.FSetBridge]
DepOfNodep.filter [definition, in Coq.FSets.FSetBridge]
DepOfNodep.fold [definition, in Coq.FSets.FSetBridge]
DepOfNodep.For_all [definition, in Coq.FSets.FSetBridge]
DepOfNodep.for_all [definition, in Coq.FSets.FSetBridge]
DepOfNodep.In [definition, in Coq.FSets.FSetBridge]
DepOfNodep.inter [definition, in Coq.FSets.FSetBridge]
DepOfNodep.is_empty [definition, in Coq.FSets.FSetBridge]
DepOfNodep.lt [definition, in Coq.FSets.FSetBridge]
DepOfNodep.lt_not_eq [definition, in Coq.FSets.FSetBridge]
DepOfNodep.lt_trans [definition, in Coq.FSets.FSetBridge]
DepOfNodep.max_elt [definition, in Coq.FSets.FSetBridge]
DepOfNodep.mem [definition, in Coq.FSets.FSetBridge]
DepOfNodep.min_elt [definition, in Coq.FSets.FSetBridge]
DepOfNodep.partition [definition, in Coq.FSets.FSetBridge]
DepOfNodep.remove [definition, in Coq.FSets.FSetBridge]
DepOfNodep.singleton [definition, in Coq.FSets.FSetBridge]
DepOfNodep.Subset [definition, in Coq.FSets.FSetBridge]
DepOfNodep.subset [definition, in Coq.FSets.FSetBridge]
DepOfNodep.t [definition, in Coq.FSets.FSetBridge]
DepOfNodep.union [definition, in Coq.FSets.FSetBridge]
depth:677 [binder, in Coq.MSets.MSetRBT]
dep_iff_non_dep_functional_rel_reification [lemma, in Coq.Logic.ChoiceFacts]
dep_non_dep_functional_rel_reification [lemma, in Coq.Logic.ChoiceFacts]
dep_non_dep_functional_choice [lemma, in Coq.Logic.ChoiceFacts]
derivable [definition, in Coq.Reals.Ranalysis1]
derivable_pow [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_pow [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_pow [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_pow_pos [lemma, in Coq.Reals.Ranalysis1]
derivable_Rsqr [lemma, in Coq.Reals.Ranalysis1]
derivable_scal [lemma, in Coq.Reals.Ranalysis1]
derivable_const [lemma, in Coq.Reals.Ranalysis1]
derivable_mult [lemma, in Coq.Reals.Ranalysis1]
derivable_minus [lemma, in Coq.Reals.Ranalysis1]
derivable_plus [lemma, in Coq.Reals.Ranalysis1]
derivable_mirr [lemma, in Coq.Reals.Ranalysis1]
derivable_opp [lemma, in Coq.Reals.Ranalysis1]
derivable_comp [lemma, in Coq.Reals.Ranalysis1]
derivable_id [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_Rsqr [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_scal [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_const [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_mult [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_minus [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_plus [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_mirr_prem [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_mirr_rev [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_mirr [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_opp_rev [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_opp [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_xeq [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_comp [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_id [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_Rsqr [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_scal_right [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_div_scal [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_scal [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_const [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_mult [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_minus [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_plus [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_mirr_rev [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_mirr_fwd [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_opp_rev [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_opp_fwd [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_opp [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_comp [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_id [lemma, in Coq.Reals.Ranalysis1]
derivable_continuous [lemma, in Coq.Reals.Ranalysis1]
derivable_continuous_pt [lemma, in Coq.Reals.Ranalysis1]
derivable_derive [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_locally_ext [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_ext [lemma, in Coq.Reals.Ranalysis1]
derivable_pt_lim_D_in [lemma, in Coq.Reals.Ranalysis1]
derivable_pt [definition, in Coq.Reals.Ranalysis1]
derivable_pt_abs [definition, in Coq.Reals.Ranalysis1]
derivable_pt_lim [definition, in Coq.Reals.Ranalysis1]
derivable_pt_sqrt [lemma, in Coq.Reals.Sqrt_reg]
derivable_pt_lim_sqrt [lemma, in Coq.Reals.Sqrt_reg]
derivable_cos [lemma, in Coq.Reals.Rtrigo_reg]
derivable_sin [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_cos [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_sin [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_cos [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_sin [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_cos_0 [lemma, in Coq.Reals.Rtrigo_reg]
derivable_pt_lim_sin_0 [lemma, in Coq.Reals.Rtrigo_reg]
derivable_sinh [lemma, in Coq.Reals.Ranalysis4]
derivable_cosh [lemma, in Coq.Reals.Ranalysis4]
derivable_exp [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_sinh [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_cosh [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_exp [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_lim_sinh [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_lim_cosh [lemma, in Coq.Reals.Ranalysis4]
derivable_finite_sum [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_finite_sum [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_lim_finite_sum [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_lim_fs [lemma, in Coq.Reals.Ranalysis4]
derivable_inv [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_inv [lemma, in Coq.Reals.Ranalysis4]
derivable_pt_lim_exp [lemma, in Coq.Reals.Exp_prop]
derivable_pt_lim_exp_0 [lemma, in Coq.Reals.Exp_prop]
derivable_pt_lim_arcsinh [lemma, in Coq.Reals.Rpower]
derivable_pt_lim_power [lemma, in Coq.Reals.Rpower]
derivable_pt_lim_ln [lemma, in Coq.Reals.Rpower]
derivable_div [lemma, in Coq.Reals.Ranalysis3]
derivable_pt_div [lemma, in Coq.Reals.Ranalysis3]
derivable_pt_lim_div [lemma, in Coq.Reals.Ranalysis3]
derivable_pt_acos [lemma, in Coq.Reals.Ratan]
derivable_pt_asin [lemma, in Coq.Reals.Ratan]
derivable_pt_ps_atan [lemma, in Coq.Reals.Ratan]
derivable_pt_lim_ps_atan [lemma, in Coq.Reals.Ratan]
derivable_pt_lim_atan [lemma, in Coq.Reals.Ratan]
derivable_pt_atan [lemma, in Coq.Reals.Ratan]
derivable_pt_tan [lemma, in Coq.Reals.Ratan]
derivable_pt_lim_CVU [lemma, in Coq.Reals.Ranalysis5]
derivable_pt_recip_interv_decr [lemma, in Coq.Reals.Ranalysis5]
derivable_pt_recip_interv [lemma, in Coq.Reals.Ranalysis5]
derivable_pt_recip_interv_prelim1_decr [lemma, in Coq.Reals.Ranalysis5]
derivable_pt_recip_interv_prelim1 [lemma, in Coq.Reals.Ranalysis5]
derivable_pt_recip_interv_prelim0 [lemma, in Coq.Reals.Ranalysis5]
derivable_pt_lim_recip_interv [lemma, in Coq.Reals.Ranalysis5]
derivable_pt_id_interv [lemma, in Coq.Reals.Ranalysis5]
derive [definition, in Coq.Reals.Ranalysis1]
Derive [library]
derive_pt_pow [lemma, in Coq.Reals.Ranalysis1]
derive_pt_Rsqr [lemma, in Coq.Reals.Ranalysis1]
derive_pt_scal [lemma, in Coq.Reals.Ranalysis1]
derive_pt_const [lemma, in Coq.Reals.Ranalysis1]
derive_pt_mult [lemma, in Coq.Reals.Ranalysis1]
derive_pt_minus [lemma, in Coq.Reals.Ranalysis1]
derive_pt_plus [lemma, in Coq.Reals.Ranalysis1]
derive_pt_mirr_rev [lemma, in Coq.Reals.Ranalysis1]
derive_pt_mirr [lemma, in Coq.Reals.Ranalysis1]
derive_pt_opp_rev [lemma, in Coq.Reals.Ranalysis1]
derive_pt_opp [lemma, in Coq.Reals.Ranalysis1]
derive_pt_comp [lemma, in Coq.Reals.Ranalysis1]
derive_pt_id [lemma, in Coq.Reals.Ranalysis1]
derive_pt_D_in [lemma, in Coq.Reals.Ranalysis1]
derive_pt_eq_1 [lemma, in Coq.Reals.Ranalysis1]
derive_pt_eq_0 [lemma, in Coq.Reals.Ranalysis1]
derive_pt_eq [lemma, in Coq.Reals.Ranalysis1]
derive_pt [definition, in Coq.Reals.Ranalysis1]
derive_pt_sqrt [lemma, in Coq.Reals.Sqrt_reg]
derive_pt_cos [lemma, in Coq.Reals.Rtrigo_reg]
derive_pt_sin [lemma, in Coq.Reals.Rtrigo_reg]
derive_pt_sinh [lemma, in Coq.Reals.Ranalysis4]
derive_pt_cosh [lemma, in Coq.Reals.Ranalysis4]
derive_pt_exp [lemma, in Coq.Reals.Ranalysis4]
derive_pt_inv [lemma, in Coq.Reals.Ranalysis4]
derive_increasing_interv_var [lemma, in Coq.Reals.MVT]
derive_increasing_interv [lemma, in Coq.Reals.MVT]
derive_increasing_interv_ax [lemma, in Coq.Reals.MVT]
derive_pt_div [lemma, in Coq.Reals.Ranalysis3]
derive_pt_acos [lemma, in Coq.Reals.Ratan]
derive_pt_asin [lemma, in Coq.Reals.Ratan]
derive_pt_atan [lemma, in Coq.Reals.Ratan]
derive_increasing_interv [lemma, in Coq.Reals.Ratan]
derive_pt_tan [lemma, in Coq.Reals.Ratan]
derive_pt_recip_interv_decr [lemma, in Coq.Reals.Ranalysis5]
derive_pt_recip_interv [lemma, in Coq.Reals.Ranalysis5]
derive_pt_recip_interv_prelim1_1_decr [lemma, in Coq.Reals.Ranalysis5]
derive_pt_recip_interv_prelim1_1 [lemma, in Coq.Reals.Ranalysis5]
derive_pt_recip_interv_prelim1_0 [lemma, in Coq.Reals.Ranalysis5]
derive_pt_recip_interv_prelim0 [lemma, in Coq.Reals.Ranalysis5]
deriv_constant2 [lemma, in Coq.Reals.Ranalysis1]
deriv_minimum [lemma, in Coq.Reals.Ranalysis1]
deriv_maximum [lemma, in Coq.Reals.Ranalysis1]
Desc [inductive, in Coq.Relations.Relation_Operators]
Descl [abbreviation, in Coq.Wellfounded.Lexicographic_Exponentiation]
description [definition, in Coq.Logic.ClassicalDescription]
Description [library]
description_rel_choice_imp_funct_choice [abbreviation, in Coq.Logic.ChoiceFacts]
desc_end [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
desc_tail [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
desc_prefix [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
destruct_list [lemma, in Coq.Lists.List]
devil:20 [binder, in Coq.Vectors.VectorDef]
devil:21 [binder, in Coq.Vectors.VectorDef]
devil:27 [binder, in Coq.Vectors.VectorDef]
devil:38 [binder, in Coq.Vectors.VectorDef]
devil:49 [binder, in Coq.Vectors.VectorDef]
devil:8 [binder, in Coq.Vectors.Fin]
devil:9 [binder, in Coq.Vectors.Fin]
dexpr:174 [binder, in Coq.Reals.Rderiv]
Df [constructor, in Coq.Init.Hexadecimal]
Df_neq:432 [binder, in Coq.Reals.Ranalysis5]
Df_neq:415 [binder, in Coq.Reals.Ranalysis5]
df:108 [binder, in Coq.Reals.Rderiv]
Df:112 [binder, in Coq.Reals.Rlimit]
df:113 [binder, in Coq.Reals.Rderiv]
Df:141 [binder, in Coq.Reals.Rderiv]
df:143 [binder, in Coq.Reals.Rderiv]
df:183 [binder, in Coq.Reals.Ranalysis1]
df:187 [binder, in Coq.Reals.Ranalysis1]
Df:43 [binder, in Coq.Reals.Rlimit]
df:62 [binder, in Coq.Reals.Rderiv]
df:74 [binder, in Coq.Reals.Rderiv]
df:95 [binder, in Coq.Reals.Rderiv]
Dgf [definition, in Coq.Reals.Rlimit]
Dg:113 [binder, in Coq.Reals.Rlimit]
dg:114 [binder, in Coq.Reals.Rderiv]
Dg:142 [binder, in Coq.Reals.Rderiv]
dg:144 [binder, in Coq.Reals.Rderiv]
Dg:44 [binder, in Coq.Reals.Rlimit]
dg:63 [binder, in Coq.Reals.Rderiv]
dg:75 [binder, in Coq.Reals.Rderiv]
Diaconescu [library]
diagonal_inverse2 [lemma, in Coq.Logic.ExtensionalityFacts]
diagonal_inverse1 [lemma, in Coq.Logic.ExtensionalityFacts]
diagonal_projs_same_behavior [lemma, in Coq.Logic.ExtensionalityFacts]
Dichotomy_ub [definition, in Coq.Reals.Rsqrt_def]
Dichotomy_lb [definition, in Coq.Reals.Rsqrt_def]
dicho_up_car [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb_car [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb_dicho_up [lemma, in Coq.Reals.Rsqrt_def]
dicho_up_cv [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb_cv [lemma, in Coq.Reals.Rsqrt_def]
dicho_up_min [lemma, in Coq.Reals.Rsqrt_def]
dicho_up_min_x [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb_maj [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb_maj_y [lemma, in Coq.Reals.Rsqrt_def]
dicho_up_decreasing [lemma, in Coq.Reals.Rsqrt_def]
dicho_lb_growing [lemma, in Coq.Reals.Rsqrt_def]
dicho_comp [lemma, in Coq.Reals.Rsqrt_def]
dicho_up [definition, in Coq.Reals.Rsqrt_def]
dicho_lb [definition, in Coq.Reals.Rsqrt_def]
did_normalization [constructor, in Coq.Classes.Morphisms]
did_normalization [constructor, in Coq.Classes.CMorphisms]
Differential [record, in Coq.Reals.Ranalysis1]
Differential_D2 [record, in Coq.Reals.Ranalysis1]
diff_false_true [lemma, in Coq.Bool.Bool]
diff_true_false [lemma, in Coq.Bool.Bool]
diff0 [projection, in Coq.Reals.RiemannInt]
digits [definition, in Coq.Numbers.Cyclic.Int63.Int63]
digits [inductive, in Coq.Numbers.Cyclic.Int31.Int31]
digits2_pos [definition, in Coq.Floats.SpecFloat]
digits31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
digits:1 [binder, in Coq.Numbers.Cyclic.Abstract.DoubleType]
dimemo_get_correct [lemma, in Coq.Lists.StreamMemo]
dimemo_list [definition, in Coq.Lists.StreamMemo]
Directed [inductive, in Coq.Sets.Cpo]
disc [definition, in Coq.Reals.Rtopology]
discrete_nat [lemma, in Coq.Arith.Compare]
DiscrR [library]
disc_P1 [lemma, in Coq.Reals.Rtopology]
Disjoint [inductive, in Coq.Sets.Ensembles]
Disjoint_intro [constructor, in Coq.Sets.Ensembles]
Disjoint_Intersection [lemma, in Coq.Sets.Powerset_facts]
Disjoint_Union.leB [variable, in Coq.Relations.Relation_Operators]
Disjoint_Union.leA [variable, in Coq.Relations.Relation_Operators]
Disjoint_Union.B [variable, in Coq.Relations.Relation_Operators]
Disjoint_Union.A [variable, in Coq.Relations.Relation_Operators]
Disjoint_Union [section, in Coq.Relations.Relation_Operators]
Disjoint_Union [library]
Disjunct [constructor, in Coq.rtauto.Rtauto]
display_pow_linear [definition, in Coq.setoid_ring.Field_theory]
display_linear [definition, in Coq.setoid_ring.Field_theory]
dist [projection, in Coq.Reals.Rlimit]
distance_symm [lemma, in Coq.Reals.Rgeom]
distance_refl [lemma, in Coq.Reals.Rgeom]
Distributivity [lemma, in Coq.Sets.Powerset_facts]
Distributivity_l [lemma, in Coq.Sets.Powerset_facts]
Distributivity' [lemma, in Coq.Sets.Powerset_facts]
distr_rev [abbreviation, in Coq.Lists.List]
dist_Desc_concat [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
dist_aux [lemma, in Coq.Wellfounded.Lexicographic_Exponentiation]
dist_tri [projection, in Coq.Reals.Rlimit]
dist_refl [projection, in Coq.Reals.Rlimit]
dist_sym [projection, in Coq.Reals.Rlimit]
dist_pos [projection, in Coq.Reals.Rlimit]
dist_euc [definition, in Coq.Reals.Rgeom]
div [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
div [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
div [axiom, in Coq.Floats.PrimFloat]
div [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
div [definition, in Coq.Init.Nat]
diveucl [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
diveucl [inductive, in Coq.Arith.Euclid]
diveucl_21_spec_aux [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
diveucl_spec [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
diveucl_21_spec [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
diveucl_def_spec [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
diveucl_21 [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
diveucl_def [definition, in Coq.Numbers.Cyclic.Int63.Int63]
diveucl_spec_aux [lemma, in Coq.Numbers.Cyclic.Int63.Cyclic63]
divex [constructor, in Coq.Arith.Euclid]
divide [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
DivideNotation [module, in Coq.Numbers.NatInt.NZGcd]
( _ | _ ) [notation, in Coq.Numbers.NatInt.NZGcd]
divmod [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
divmod [definition, in Coq.Init.Nat]
DivMod [module, in Coq.Numbers.NatInt.NZDiv]
DivModNotation [module, in Coq.Numbers.NatInt.NZDiv]
_ mod _ [notation, in Coq.Numbers.NatInt.NZDiv]
_ / _ [notation, in Coq.Numbers.NatInt.NZDiv]
divmod_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
DivMod' [module, in Coq.Numbers.NatInt.NZDiv]
DivMod.div [axiom, in Coq.Numbers.NatInt.NZDiv]
DivMod.modulo [axiom, in Coq.Numbers.NatInt.NZDiv]
div_mod [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
div_gt [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
div_eq_inv [lemma, in Coq.Reals.Ranalysis1]
div_real_fct [definition, in Coq.Reals.Ranalysis1]
div_fct [definition, in Coq.Reals.Ranalysis1]
div_spec [axiom, in Coq.Numbers.Cyclic.Int63.Int63]
div_Zdiv [lemma, in Coq.ZArith.Zdiv]
div_lt [lemma, in Coq.Numbers.Cyclic.Int63.Cyclic63]
div_le_0 [lemma, in Coq.Numbers.Cyclic.Int63.Cyclic63]
div_eucl_th [projection, in Coq.setoid_ring.Ring_theory]
div_theory [record, in Coq.setoid_ring.Ring_theory]
div_spec [axiom, in Coq.Floats.FloatAxioms]
div2 [abbreviation, in Coq.Arith.Div2]
div2 [definition, in Coq.Init.Nat]
Div2 [library]
div2_decr [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
div2_bitwise [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
div2_double_plus_one [lemma, in Coq.Arith.Div2]
div2_double [lemma, in Coq.Arith.Div2]
div2_odd [lemma, in Coq.Arith.Div2]
div2_even [lemma, in Coq.Arith.Div2]
div2_not_R0 [lemma, in Coq.Reals.Exp_prop]
div2_S_double [lemma, in Coq.Reals.Exp_prop]
div2_double [lemma, in Coq.Reals.Exp_prop]
div2_phi [lemma, in Coq.Numbers.Cyclic.Int63.Int63]
div21 [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
div31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
div31_phi [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
div312_phi [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
div3121 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
Dln [lemma, in Coq.Reals.Rpower]
dmemo_get_correct [lemma, in Coq.Lists.StreamMemo]
dmemo_get [definition, in Coq.Lists.StreamMemo]
dmemo_list [definition, in Coq.Lists.StreamMemo]
Dminus [lemma, in Coq.Reals.Rderiv]
Dmult [lemma, in Coq.Reals.Rderiv]
Dmult_const [lemma, in Coq.Reals.Rderiv]
dm:49 [binder, in Coq.NArith.Ndist]
dnorme [definition, in Coq.Numbers.DecimalQ]
dnorme_invol [lemma, in Coq.Numbers.DecimalQ]
dnorme_spec [lemma, in Coq.Numbers.DecimalQ]
dnormf [definition, in Coq.Numbers.DecimalQ]
dnormf_invol [lemma, in Coq.Numbers.DecimalQ]
dnormf_spec [lemma, in Coq.Numbers.DecimalQ]
dn:434 [binder, in Coq.Lists.List]
DO [instance, in Coq.micromega.DeclConstant]
domain_P1 [lemma, in Coq.Reals.Rtopology]
domain_finite [definition, in Coq.Reals.Rtopology]
DoneProof [constructor, in Coq.micromega.ZMicromega]
Dopp [lemma, in Coq.Reals.Rderiv]
double [abbreviation, in Coq.Arith.Div2]
double [definition, in Coq.Init.Nat]
double [definition, in Coq.Numbers.HexadecimalZ]
double [lemma, in Coq.Reals.RIneq]
DoubleQuote [definition, in Coq.Strings.Ascii]
DoubleType [library]
double_twice [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
double_twice_plus_one_firstl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
double_twice_firstl [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
double_odd [lemma, in Coq.Arith.Div2]
double_even [lemma, in Coq.Arith.Div2]
double_plus [lemma, in Coq.Arith.Div2]
double_S [lemma, in Coq.Arith.Div2]
double_moins_un_xO_discr [abbreviation, in Coq.PArith.BinPos]
double_to_hex_int [lemma, in Coq.Numbers.HexadecimalZ]
double_norm [lemma, in Coq.Numbers.HexadecimalZ]
double_var [lemma, in Coq.Reals.RIneq]
down:12 [binder, in Coq.Reals.Rsqrt_def]
down:16 [binder, in Coq.Reals.Rsqrt_def]
do_subrelation [constructor, in Coq.Classes.Morphisms]
do_subrelation [constructor, in Coq.Classes.CMorphisms]
Dpower [lemma, in Coq.Reals.Rpower]
DQ [instance, in Coq.micromega.DeclConstant]
DReal [definition, in Coq.Reals.ClassicalDedekindReals]
DRealAbstr [definition, in Coq.Reals.ClassicalDedekindReals]
DRealAbstrFalse [lemma, in Coq.Reals.ClassicalDedekindReals]
DRealConstructive [definition, in Coq.Reals.ClassicalConstructiveReals]
DRealOpen [lemma, in Coq.Reals.ClassicalDedekindReals]
DRealQlim [definition, in Coq.Reals.ClassicalDedekindReals]
DRealQlim_rec [definition, in Coq.Reals.ClassicalDedekindReals]
DRealQuot1 [lemma, in Coq.Reals.ClassicalDedekindReals]
DRealQuot2 [lemma, in Coq.Reals.ClassicalDedekindReals]
DRealRepr [definition, in Coq.Reals.ClassicalDedekindReals]
DRealReprQ [lemma, in Coq.Reals.ClassicalDedekindReals]
DRealReprQup [lemma, in Coq.Reals.ClassicalDedekindReals]
DrinkerParadox [definition, in Coq.Logic.ClassicalFacts]
DS [instance, in Coq.micromega.DeclConstant]
DSO_to_OT [module, in Coq.Structures.Orders]
dummy_can_compute_Z [projection, in Coq.nsatz.Nsatz]
dummy_can_compute_Z [constructor, in Coq.nsatz.Nsatz]
Dx [lemma, in Coq.Reals.Rderiv]
DxH [instance, in Coq.micromega.DeclConstant]
DxI [instance, in Coq.micromega.DeclConstant]
DxO [instance, in Coq.micromega.DeclConstant]
Dx_pow_n [lemma, in Coq.Reals.Rderiv]
DZneg [instance, in Coq.micromega.DeclConstant]
DZO [instance, in Coq.micromega.DeclConstant]
DZpos [instance, in Coq.micromega.DeclConstant]
DZpow [instance, in Coq.micromega.DeclConstant]
DZpow_pos [instance, in Coq.micromega.DeclConstant]
D_pow_n [lemma, in Coq.Reals.Rderiv]
D_in [definition, in Coq.Reals.Rderiv]
D_x [definition, in Coq.Reals.Rderiv]
D_x_no_cond [lemma, in Coq.Reals.Ranalysis2]
d_rev:36 [binder, in Coq.Init.Decimal]
d_rev:36 [binder, in Coq.Init.Hexadecimal]
D_in_ext [lemma, in Coq.Reals.Rpower]
D_in_imp [lemma, in Coq.Reals.Rpower]
d_conc [constructor, in Coq.Relations.Relation_Operators]
d_one [constructor, in Coq.Relations.Relation_Operators]
d_nil [constructor, in Coq.Relations.Relation_Operators]
D_Or [constructor, in Coq.rtauto.Rtauto]
D_And [constructor, in Coq.rtauto.Rtauto]
D_Arrow [constructor, in Coq.rtauto.Rtauto]
d'':11 [binder, in Coq.Numbers.DecimalFacts]
d'':26 [binder, in Coq.NArith.Ndist]
d'':38 [binder, in Coq.NArith.Ndist]
d'':50 [binder, in Coq.NArith.Ndist]
d'':9 [binder, in Coq.Numbers.HexadecimalFacts]
d':10 [binder, in Coq.Numbers.DecimalFacts]
d':11 [binder, in Coq.Numbers.DecimalN]
d':11 [binder, in Coq.Numbers.DecimalZ]
d':11 [binder, in Coq.Numbers.HexadecimalZ]
d':11 [binder, in Coq.Numbers.HexadecimalN]
d':12 [binder, in Coq.Numbers.HexadecimalFacts]
d':13 [binder, in Coq.Numbers.HexadecimalPos]
d':13 [binder, in Coq.Numbers.DecimalPos]
d':14 [binder, in Coq.Numbers.DecimalFacts]
d':145 [binder, in Coq.Lists.List]
d':150 [binder, in Coq.FSets.FMapAVL]
d':170 [binder, in Coq.Lists.List]
d':18 [binder, in Coq.NArith.Ndist]
d':2 [binder, in Coq.Numbers.DecimalFacts]
d':2 [binder, in Coq.Numbers.HexadecimalFacts]
d':21 [binder, in Coq.Numbers.DecimalN]
d':21 [binder, in Coq.Numbers.HexadecimalN]
d':23 [binder, in Coq.NArith.Ndist]
d':23 [binder, in Coq.Numbers.HexadecimalNat]
d':23 [binder, in Coq.Numbers.DecimalNat]
d':25 [binder, in Coq.NArith.Ndist]
d':26 [binder, in Coq.Init.Decimal]
d':26 [binder, in Coq.Init.Hexadecimal]
d':27 [binder, in Coq.Numbers.HexadecimalFacts]
d':30 [binder, in Coq.Numbers.HexadecimalFacts]
d':31 [binder, in Coq.Init.Decimal]
d':31 [binder, in Coq.Init.Hexadecimal]
d':32 [binder, in Coq.NArith.Ndist]
d':34 [binder, in Coq.Numbers.DecimalFacts]
d':35 [binder, in Coq.NArith.Ndist]
d':36 [binder, in Coq.Numbers.HexadecimalFacts]
d':37 [binder, in Coq.Numbers.DecimalFacts]
d':37 [binder, in Coq.NArith.Ndist]
d':38 [binder, in Coq.Numbers.HexadecimalFacts]
d':39 [binder, in Coq.Numbers.HexadecimalNat]
d':39 [binder, in Coq.Numbers.DecimalNat]
d':4 [binder, in Coq.Numbers.DecimalFacts]
d':40 [binder, in Coq.NArith.Ndist]
d':41 [binder, in Coq.Numbers.HexadecimalNat]
d':41 [binder, in Coq.Numbers.DecimalNat]
d':42 [binder, in Coq.NArith.Ndist]
d':44 [binder, in Coq.NArith.Ndist]
d':45 [binder, in Coq.Numbers.HexadecimalFacts]
d':46 [binder, in Coq.NArith.Ndist]
d':48 [binder, in Coq.NArith.Ndist]
d':49 [binder, in Coq.Numbers.DecimalFacts]
d':49 [binder, in Coq.Numbers.HexadecimalFacts]
d':51 [binder, in Coq.Numbers.DecimalFacts]
d':51 [binder, in Coq.Numbers.HexadecimalNat]
d':51 [binder, in Coq.Numbers.DecimalNat]
d':57 [binder, in Coq.Numbers.HexadecimalPos]
d':57 [binder, in Coq.Numbers.DecimalPos]
d':58 [binder, in Coq.Numbers.DecimalFacts]
d':59 [binder, in Coq.Numbers.HexadecimalPos]
d':59 [binder, in Coq.Numbers.DecimalPos]
d':61 [binder, in Coq.Numbers.HexadecimalFacts]
d':62 [binder, in Coq.Numbers.DecimalFacts]
d':63 [binder, in Coq.Numbers.HexadecimalFacts]
d':642 [binder, in Coq.ssr.ssrbool]
d':647 [binder, in Coq.ssr.ssrbool]
d':65 [binder, in Coq.Numbers.HexadecimalFacts]
d':655 [binder, in Coq.ssr.ssrbool]
d':661 [binder, in Coq.ssr.ssrbool]
d':7 [binder, in Coq.Numbers.DecimalString]
d':7 [binder, in Coq.Numbers.HexadecimalString]
d':71 [binder, in Coq.Numbers.HexadecimalQ]
d':72 [binder, in Coq.Numbers.DecimalPos]
d':73 [binder, in Coq.Numbers.HexadecimalQ]
d':76 [binder, in Coq.Numbers.HexadecimalPos]
d':8 [binder, in Coq.Numbers.HexadecimalFacts]
d':88 [binder, in Coq.Numbers.DecimalFacts]
d':9 [binder, in Coq.Numbers.DecimalN]
d':9 [binder, in Coq.Numbers.DecimalZ]
d':9 [binder, in Coq.Numbers.HexadecimalZ]
d':9 [binder, in Coq.Numbers.HexadecimalN]
d':90 [binder, in Coq.Numbers.DecimalFacts]
d':92 [binder, in Coq.Numbers.DecimalFacts]
d':95 [binder, in Coq.ZArith.Znumtheory]
D0 [constructor, in Coq.Init.Decimal]
D0 [constructor, in Coq.Init.Hexadecimal]
D0 [constructor, in Coq.Numbers.Cyclic.Int31.Int31]
d1 [projection, in Coq.Reals.Ranalysis1]
D1 [constructor, in Coq.Init.Decimal]
D1 [constructor, in Coq.Init.Hexadecimal]
D1 [constructor, in Coq.Numbers.Cyclic.Int31.Int31]
D1':638 [binder, in Coq.ssr.ssrbool]
d1':653 [binder, in Coq.ssr.ssrbool]
D1:1 [binder, in Coq.Reals.Rtopology]
D1:101 [binder, in Coq.Reals.Rpower]
d1:101 [binder, in Coq.FSets.FMapAVL]
d1:112 [binder, in Coq.Floats.SpecFloat]
d1:1247 [binder, in Coq.FSets.FMapAVL]
D1:125 [binder, in Coq.Reals.Rtopology]
d1:1253 [binder, in Coq.FSets.FMapAVL]
D1:15 [binder, in Coq.Reals.Rtopology]
d1:1510 [binder, in Coq.FSets.FMapAVL]
d1:1530 [binder, in Coq.FSets.FMapAVL]
d1:1536 [binder, in Coq.FSets.FMapAVL]
D1:18 [binder, in Coq.Reals.Rtopology]
d1:224 [binder, in Coq.Reals.Ranalysis5]
d1:228 [binder, in Coq.Reals.Ranalysis5]
d1:32 [binder, in Coq.Init.Decimal]
d1:32 [binder, in Coq.Init.Hexadecimal]
D1:32 [binder, in Coq.Reals.Rtopology]
d1:353 [binder, in Coq.FSets.FMapFullAVL]
D1:48 [binder, in Coq.Reals.Rtopology]
D1:52 [binder, in Coq.Reals.Rtopology]
D1:55 [binder, in Coq.Reals.Rtopology]
D1:57 [binder, in Coq.Reals.Rtopology]
d1:652 [binder, in Coq.ssr.ssrbool]
D1:75 [binder, in Coq.Reals.Rpower]
d2 [projection, in Coq.Reals.Ranalysis1]
D2 [constructor, in Coq.Init.Decimal]
D2 [constructor, in Coq.Init.Hexadecimal]
D2':639 [binder, in Coq.ssr.ssrbool]
d2:113 [binder, in Coq.Floats.SpecFloat]
d2:1248 [binder, in Coq.FSets.FMapAVL]
d2:1256 [binder, in Coq.FSets.FMapAVL]
D2:126 [binder, in Coq.Reals.Rtopology]
d2:1531 [binder, in Coq.FSets.FMapAVL]
d2:1539 [binder, in Coq.FSets.FMapAVL]
D2:16 [binder, in Coq.Reals.Rtopology]
D2:19 [binder, in Coq.Reals.Rtopology]
D2:2 [binder, in Coq.Reals.Rtopology]
d2:225 [binder, in Coq.Reals.Ranalysis5]
d2:229 [binder, in Coq.Reals.Ranalysis5]
d2:33 [binder, in Coq.Init.Decimal]
d2:33 [binder, in Coq.Init.Hexadecimal]
D2:33 [binder, in Coq.Reals.Rtopology]
d2:354 [binder, in Coq.FSets.FMapFullAVL]
D2:49 [binder, in Coq.Reals.Rtopology]
D2:53 [binder, in Coq.Reals.Rtopology]
D2:56 [binder, in Coq.Reals.Rtopology]
D2:58 [binder, in Coq.Reals.Rtopology]
D3 [constructor, in Coq.Init.Decimal]
D3 [constructor, in Coq.Init.Hexadecimal]
d3':663 [binder, in Coq.ssr.ssrbool]
D3:34 [binder, in Coq.Reals.Rtopology]
d3:662 [binder, in Coq.ssr.ssrbool]
D4 [constructor, in Coq.Init.Decimal]
D4 [constructor, in Coq.Init.Hexadecimal]
D5 [constructor, in Coq.Init.Decimal]
D5 [constructor, in Coq.Init.Hexadecimal]
D6 [constructor, in Coq.Init.Decimal]
D6 [constructor, in Coq.Init.Hexadecimal]
D7 [constructor, in Coq.Init.Decimal]
D7 [constructor, in Coq.Init.Hexadecimal]
D8 [constructor, in Coq.Init.Decimal]
D8 [constructor, in Coq.Init.Hexadecimal]
D9 [constructor, in Coq.Init.Decimal]
D9 [constructor, in Coq.Init.Hexadecimal]
D:1 [binder, in Coq.Reals.Rderiv]
d:1 [binder, in Coq.Numbers.DecimalFacts]
d:1 [binder, in Coq.Numbers.HexadecimalPos]
d:1 [binder, in Coq.Numbers.HexadecimalNat]
d:1 [binder, in Coq.Numbers.HexadecimalFacts]
d:1 [binder, in Coq.Numbers.DecimalPos]
d:1 [binder, in Coq.Numbers.DecimalNat]
d:10 [binder, in Coq.Numbers.DecimalQ]
d:10 [binder, in Coq.QArith.Qabs]
d:10 [binder, in Coq.Numbers.DecimalN]
d:10 [binder, in Coq.Numbers.DecimalZ]
d:10 [binder, in Coq.Numbers.HexadecimalFacts]
d:10 [binder, in Coq.Numbers.HexadecimalZ]
d:10 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
D:10 [binder, in Coq.Reals.Rtopology]
d:10 [binder, in Coq.Numbers.HexadecimalN]
D:10 [binder, in Coq.Program.Combinators]
D:100 [binder, in Coq.Reals.Rpower]
D:100 [binder, in Coq.Reals.Rlimit]
D:101 [binder, in Coq.Reals.Rtopology]
d:1020 [binder, in Coq.FSets.FMapAVL]
d:1024 [binder, in Coq.FSets.FMapAVL]
d:104 [binder, in Coq.setoid_ring.Field_theory]
d:105 [binder, in Coq.ZArith.Znumtheory]
D:106 [binder, in Coq.Reals.Rderiv]
D:107 [binder, in Coq.Reals.Rpower]
D:107 [binder, in Coq.Reals.Rtopology]
d:109 [binder, in Coq.ZArith.Znumtheory]
d:109 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
d:11 [binder, in Coq.Init.Numeral]
d:11 [binder, in Coq.Numbers.HexadecimalNat]
d:11 [binder, in Coq.Numbers.HexadecimalFacts]
d:11 [binder, in Coq.Numbers.DecimalNat]
d:111 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
D:112 [binder, in Coq.Reals.Rderiv]
D:112 [binder, in Coq.Reals.Rtopology]
D:112 [binder, in Coq.Reals.Ranalysis5]
D:114 [binder, in Coq.Reals.Rtopology]
d:114 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
d:1140 [binder, in Coq.FSets.FMapAVL]
d:1145 [binder, in Coq.FSets.FMapAVL]
d:1149 [binder, in Coq.FSets.FMapAVL]
d:116 [binder, in Coq.Lists.List]
d:119 [binder, in Coq.Lists.List]
D:119 [binder, in Coq.Reals.Rlimit]
d:12 [binder, in Coq.Numbers.DecimalFacts]
d:12 [binder, in Coq.Numbers.HexadecimalPos]
d:12 [binder, in Coq.Numbers.DecimalQ]
d:12 [binder, in Coq.Numbers.DecimalZ]
d:12 [binder, in Coq.Numbers.HexadecimalZ]
D:12 [binder, in Coq.Reals.Rtopology]
d:12 [binder, in Coq.Numbers.DecimalPos]
d:121 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
D:121 [binder, in Coq.Reals.Rtopology]
d:123 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
d:1235 [binder, in Coq.FSets.FMapAVL]
d:124 [binder, in Coq.Floats.SpecFloat]
D:125 [binder, in Coq.Reals.Rderiv]
d:125 [binder, in Coq.NArith.BinNatDef]
d:125 [binder, in Coq.ZArith.Znumtheory]
d:126 [binder, in Coq.NArith.BinNatDef]
d:127 [binder, in Coq.NArith.BinNatDef]
d:129 [binder, in Coq.NArith.BinNatDef]
d:13 [binder, in Coq.Reals.Rderiv]
d:13 [binder, in Coq.Numbers.DecimalFacts]
d:13 [binder, in Coq.Numbers.DecimalQ]
d:13 [binder, in Coq.Numbers.DecimalN]
d:13 [binder, in Coq.Numbers.HexadecimalN]
d:130 [binder, in Coq.NArith.BinNatDef]
d:1301 [binder, in Coq.FSets.FMapAVL]
d:1305 [binder, in Coq.FSets.FMapAVL]
d:131 [binder, in Coq.Lists.List]
d:131 [binder, in Coq.NArith.BinNatDef]
d:1317 [binder, in Coq.FSets.FMapAVL]
d:134 [binder, in Coq.Lists.List]
d:137 [binder, in Coq.Lists.List]
d:138 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
D:14 [binder, in Coq.Reals.Rderiv]
d:14 [binder, in Coq.Init.Decimal]
d:14 [binder, in Coq.Numbers.DecimalString]
d:14 [binder, in Coq.Init.Hexadecimal]
d:14 [binder, in Coq.Numbers.DecimalZ]
d:14 [binder, in Coq.Numbers.HexadecimalString]
d:14 [binder, in Coq.Numbers.HexadecimalZ]
D:14 [binder, in Coq.Reals.Rtopology]
d:14 [binder, in Coq.Numbers.HexadecimalQ]
d:141 [binder, in Coq.Floats.SpecFloat]
d:141 [binder, in Coq.Lists.List]
d:144 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
d:144 [binder, in Coq.Lists.List]
d:145 [binder, in Coq.Floats.SpecFloat]
d:145 [binder, in Coq.Reals.PSeries_reg]
d:148 [binder, in Coq.Lists.List]
d:151 [binder, in Coq.FSets.FMapAVL]
d:152 [binder, in Coq.Lists.List]
d:152 [binder, in Coq.FSets.FMapAVL]
d:152 [binder, in Coq.Reals.PSeries_reg]
d:156 [binder, in Coq.Lists.List]
d:159 [binder, in Coq.Reals.PSeries_reg]
d:16 [binder, in Coq.Numbers.HexadecimalNat]
d:16 [binder, in Coq.Numbers.HexadecimalFacts]
d:16 [binder, in Coq.Numbers.HexadecimalZ]
d:16 [binder, in Coq.Numbers.DecimalNat]
d:161 [binder, in Coq.Lists.List]
D:161 [binder, in Coq.Reals.Rtopology]
d:164 [binder, in Coq.Lists.List]
D:164 [binder, in Coq.Reals.Rtopology]
d:169 [binder, in Coq.Lists.List]
d:17 [binder, in Coq.Init.Decimal]
d:17 [binder, in Coq.NArith.Ndist]
d:17 [binder, in Coq.Init.Hexadecimal]
d:17 [binder, in Coq.Numbers.DecimalN]
d:17 [binder, in Coq.Numbers.HexadecimalN]
D:171 [binder, in Coq.Reals.Rderiv]
d:178 [binder, in Coq.PArith.BinPosDef]
d:18 [binder, in Coq.Numbers.DecimalString]
d:18 [binder, in Coq.Numbers.DecimalQ]
d:18 [binder, in Coq.Numbers.HexadecimalString]
d:18 [binder, in Coq.Numbers.HexadecimalZ]
d:182 [binder, in Coq.PArith.BinPosDef]
d:185 [binder, in Coq.PArith.BinPosDef]
d:189 [binder, in Coq.PArith.BinPosDef]
d:19 [binder, in Coq.Numbers.HexadecimalNat]
d:19 [binder, in Coq.Numbers.DecimalN]
d:19 [binder, in Coq.Numbers.HexadecimalN]
d:19 [binder, in Coq.Numbers.DecimalNat]
d:192 [binder, in Coq.PArith.BinPosDef]
d:194 [binder, in Coq.PArith.BinPosDef]
d:196 [binder, in Coq.Lists.List]
d:196 [binder, in Coq.PArith.BinPosDef]
d:198 [binder, in Coq.PArith.BinPosDef]
d:199 [binder, in Coq.Lists.List]
d:2 [binder, in Coq.Numbers.DecimalString]
d:2 [binder, in Coq.Numbers.DecimalQ]
d:2 [binder, in Coq.Numbers.DecimalN]
d:2 [binder, in Coq.Numbers.DecimalZ]
d:2 [binder, in Coq.Numbers.HexadecimalString]
d:2 [binder, in Coq.Numbers.HexadecimalZ]
d:2 [binder, in Coq.Numbers.HexadecimalN]
d:2 [binder, in Coq.Numbers.HexadecimalQ]
d:20 [binder, in Coq.Init.Decimal]
d:20 [binder, in Coq.Numbers.DecimalString]
d:20 [binder, in Coq.Numbers.HexadecimalPos]
d:20 [binder, in Coq.Init.Hexadecimal]
d:20 [binder, in Coq.Lists.ListDec]
d:20 [binder, in Coq.Numbers.HexadecimalNat]
d:20 [binder, in Coq.Numbers.DecimalN]
D:20 [binder, in Coq.Classes.CMorphisms]
d:20 [binder, in Coq.Numbers.HexadecimalString]
d:20 [binder, in Coq.Numbers.HexadecimalN]
d:20 [binder, in Coq.Numbers.DecimalPos]
d:20 [binder, in Coq.Numbers.DecimalNat]
d:201 [binder, in Coq.Lists.List]
D:201 [binder, in Coq.Reals.Rtopology]
d:206 [binder, in Coq.Lists.List]
d:208 [binder, in Coq.Reals.Rfunctions]
d:21 [binder, in Coq.Init.Decimal]
d:21 [binder, in Coq.Numbers.DecimalFacts]
d:21 [binder, in Coq.Numbers.DecimalString]
D:21 [binder, in Coq.Classes.Morphisms]
d:21 [binder, in Coq.NArith.Ndist]
d:21 [binder, in Coq.Init.Hexadecimal]
d:21 [binder, in Coq.Numbers.HexadecimalString]
d:21 [binder, in Coq.Numbers.HexadecimalZ]
D:21 [binder, in Coq.Reals.Rtopology]
d:211 [binder, in Coq.Lists.List]
d:22 [binder, in Coq.Numbers.HexadecimalPos]
d:22 [binder, in Coq.NArith.Ndist]
d:22 [binder, in Coq.Numbers.HexadecimalNat]
d:22 [binder, in Coq.Numbers.DecimalPos]
d:22 [binder, in Coq.Numbers.DecimalNat]
d:23 [binder, in Coq.Init.Decimal]
d:23 [binder, in Coq.Numbers.DecimalString]
d:23 [binder, in Coq.Init.Hexadecimal]
d:23 [binder, in Coq.Numbers.HexadecimalString]
D:23 [binder, in Coq.Reals.Rtopology]
d:233 [binder, in Coq.Sorting.Permutation]
d:24 [binder, in Coq.Numbers.DecimalString]
d:24 [binder, in Coq.Numbers.HexadecimalPos]
d:24 [binder, in Coq.NArith.Ndist]
d:24 [binder, in Coq.Numbers.HexadecimalString]
D:24 [binder, in Coq.Reals.Rtopology]
d:24 [binder, in Coq.Numbers.DecimalPos]
d:242 [binder, in Coq.micromega.Tauto]
d:25 [binder, in Coq.Init.Decimal]
d:25 [binder, in Coq.Numbers.HexadecimalPos]
d:25 [binder, in Coq.Numbers.DecimalQ]
d:25 [binder, in Coq.Init.Hexadecimal]
d:25 [binder, in Coq.Lists.ListDec]
d:25 [binder, in Coq.Numbers.HexadecimalNat]
D:25 [binder, in Coq.Reals.Rtopology]
d:25 [binder, in Coq.Numbers.DecimalPos]
d:25 [binder, in Coq.Numbers.DecimalNat]
d:26 [binder, in Coq.Numbers.HexadecimalPos]
d:26 [binder, in Coq.Numbers.DecimalQ]
d:26 [binder, in Coq.Numbers.HexadecimalNat]
d:26 [binder, in Coq.FSets.FMapAVL]
d:26 [binder, in Coq.Numbers.HexadecimalFacts]
d:26 [binder, in Coq.Numbers.DecimalPos]
d:26 [binder, in Coq.Numbers.DecimalNat]
d:27 [binder, in Coq.Numbers.HexadecimalPos]
d:27 [binder, in Coq.Numbers.DecimalQ]
d:27 [binder, in Coq.NArith.Ndist]
d:27 [binder, in Coq.Numbers.DecimalPos]
d:27 [binder, in Coq.Logic.FinFun]
d:28 [binder, in Coq.Numbers.DecimalString]
d:28 [binder, in Coq.Numbers.HexadecimalPos]
d:28 [binder, in Coq.Numbers.DecimalQ]
d:28 [binder, in Coq.NArith.Ndist]
d:28 [binder, in Coq.Numbers.HexadecimalString]
d:28 [binder, in Coq.Numbers.DecimalPos]
d:282 [binder, in Coq.ssr.ssrbool]
d:284 [binder, in Coq.micromega.RingMicromega]
d:284 [binder, in Coq.Lists.List]
d:29 [binder, in Coq.Init.Decimal]
d:29 [binder, in Coq.NArith.Ndist]
d:29 [binder, in Coq.Init.Hexadecimal]
d:29 [binder, in Coq.Numbers.HexadecimalNat]
d:29 [binder, in Coq.Numbers.HexadecimalFacts]
D:29 [binder, in Coq.Reals.Rtopology]
d:29 [binder, in Coq.Numbers.DecimalNat]
D:292 [binder, in Coq.Reals.Rtopology]
d:3 [binder, in Coq.Numbers.DecimalFacts]
d:3 [binder, in Coq.QArith.Qabs]
d:3 [binder, in Coq.Numbers.HexadecimalNat]
d:3 [binder, in Coq.Numbers.HexadecimalFacts]
d:3 [binder, in Coq.Numbers.HexadecimalQ]
d:3 [binder, in Coq.Numbers.DecimalNat]
d:30 [binder, in Coq.Init.Decimal]
d:30 [binder, in Coq.NArith.Ndist]
d:30 [binder, in Coq.Init.Hexadecimal]
d:30 [binder, in Coq.Numbers.HexadecimalNat]
d:30 [binder, in Coq.Numbers.DecimalNat]
D:302 [binder, in Coq.Reals.Rtopology]
d:31 [binder, in Coq.NArith.Ndist]
d:31 [binder, in Coq.Numbers.HexadecimalNat]
d:31 [binder, in Coq.Numbers.HexadecimalFacts]
D:31 [binder, in Coq.Reals.Rtopology]
d:31 [binder, in Coq.Numbers.DecimalNat]
D:31 [binder, in Coq.Sorting.Heap]
D:319 [binder, in Coq.Reals.Rtopology]
d:32 [binder, in Coq.Numbers.HexadecimalPos]
d:32 [binder, in Coq.Numbers.HexadecimalNat]
d:32 [binder, in Coq.Numbers.DecimalPos]
d:32 [binder, in Coq.Numbers.DecimalNat]
D:323 [binder, in Coq.Reals.Rtopology]
d:325 [binder, in Coq.Reals.RIneq]
D:327 [binder, in Coq.Reals.Rtopology]
d:33 [binder, in Coq.Numbers.DecimalFacts]
d:33 [binder, in Coq.Numbers.HexadecimalPos]
d:33 [binder, in Coq.Numbers.DecimalQ]
d:33 [binder, in Coq.NArith.Ndist]
d:33 [binder, in Coq.Numbers.DecimalPos]
d:332 [binder, in Coq.Lists.List]
d:336 [binder, in Coq.Lists.List]
d:34 [binder, in Coq.Reals.Abstract.ConstructiveReals]
d:34 [binder, in Coq.Numbers.DecimalString]
d:34 [binder, in Coq.NArith.Ndist]
d:34 [binder, in Coq.Numbers.HexadecimalFacts]
d:34 [binder, in Coq.Numbers.HexadecimalString]
d:34 [binder, in Coq.Logic.FinFun]
d:35 [binder, in Coq.Init.Decimal]
d:35 [binder, in Coq.Numbers.DecimalString]
d:35 [binder, in Coq.Init.Hexadecimal]
d:35 [binder, in Coq.Numbers.HexadecimalNat]
d:35 [binder, in Coq.FSets.FMapAVL]
d:35 [binder, in Coq.Numbers.HexadecimalFacts]
d:35 [binder, in Coq.Numbers.HexadecimalString]
D:35 [binder, in Coq.Reals.Rtopology]
d:35 [binder, in Coq.Numbers.DecimalNat]
d:36 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
d:36 [binder, in Coq.Numbers.DecimalFacts]
d:36 [binder, in Coq.Numbers.DecimalString]
d:36 [binder, in Coq.NArith.Ndist]
d:36 [binder, in Coq.Numbers.HexadecimalString]
D:36 [binder, in Coq.Reals.Rtopology]
d:36 [binder, in Coq.QArith.QArith_base]
d:37 [binder, in Coq.Numbers.DecimalString]
d:37 [binder, in Coq.Numbers.HexadecimalNat]
d:37 [binder, in Coq.Numbers.HexadecimalFacts]
d:37 [binder, in Coq.Numbers.HexadecimalString]
D:37 [binder, in Coq.Reals.Rlimit]
d:37 [binder, in Coq.Numbers.DecimalNat]
d:38 [binder, in Coq.Numbers.HexadecimalNat]
D:38 [binder, in Coq.Reals.Rtopology]
d:38 [binder, in Coq.Numbers.DecimalNat]
d:39 [binder, in Coq.Numbers.DecimalString]
d:39 [binder, in Coq.Numbers.Natural.Abstract.NPow]
d:39 [binder, in Coq.NArith.Ndist]
d:39 [binder, in Coq.Numbers.HexadecimalFacts]
d:39 [binder, in Coq.Numbers.HexadecimalString]
D:39 [binder, in Coq.Reals.Rtopology]
d:4 [binder, in Coq.Numbers.HexadecimalPos]
d:4 [binder, in Coq.Numbers.HexadecimalFacts]
d:4 [binder, in Coq.Numbers.DecimalPos]
d:4 [binder, in Coq.Reals.ClassicalConstructiveReals]
d:4 [binder, in Coq.QArith.QArith_base]
d:40 [binder, in Coq.Numbers.HexadecimalNat]
d:40 [binder, in Coq.Numbers.HexadecimalFacts]
d:40 [binder, in Coq.Numbers.DecimalNat]
d:41 [binder, in Coq.Numbers.DecimalFacts]
d:41 [binder, in Coq.NArith.Ndist]
d:41 [binder, in Coq.FSets.FMapAVL]
d:41 [binder, in Coq.micromega.QMicromega]
d:43 [binder, in Coq.Numbers.HexadecimalPos]
d:43 [binder, in Coq.Numbers.Natural.Abstract.NPow]
d:43 [binder, in Coq.NArith.Ndist]
d:43 [binder, in Coq.Numbers.HexadecimalNat]
d:43 [binder, in Coq.micromega.QMicromega]
d:43 [binder, in Coq.Numbers.DecimalPos]
d:43 [binder, in Coq.Numbers.DecimalNat]
d:432 [binder, in Coq.Lists.List]
d:44 [binder, in Coq.Init.Decimal]
d:44 [binder, in Coq.Numbers.DecimalFacts]
d:44 [binder, in Coq.Numbers.HexadecimalPos]
d:44 [binder, in Coq.Init.Hexadecimal]
d:44 [binder, in Coq.Numbers.HexadecimalFacts]
d:44 [binder, in Coq.Numbers.DecimalPos]
d:45 [binder, in Coq.NArith.Ndist]
d:454 [binder, in Coq.Numbers.Cyclic.Int63.Int63]
d:46 [binder, in Coq.micromega.QMicromega]
d:46 [binder, in Coq.Numbers.HexadecimalFacts]
d:47 [binder, in Coq.Numbers.DecimalFacts]
d:47 [binder, in Coq.Numbers.HexadecimalPos]
d:47 [binder, in Coq.NArith.Ndist]
d:47 [binder, in Coq.Numbers.HexadecimalNat]
d:47 [binder, in Coq.Numbers.HexadecimalFacts]
d:47 [binder, in Coq.Numbers.DecimalPos]
d:47 [binder, in Coq.Numbers.DecimalNat]
D:48 [binder, in Coq.Reals.Ranalysis1]
d:48 [binder, in Coq.Numbers.DecimalFacts]
d:48 [binder, in Coq.Numbers.HexadecimalPos]
d:48 [binder, in Coq.Numbers.HexadecimalFacts]
D:48 [binder, in Coq.Reals.Rlimit]
d:48 [binder, in Coq.Numbers.DecimalPos]
d:49 [binder, in Coq.Numbers.HexadecimalNat]
d:49 [binder, in Coq.Numbers.DecimalNat]
D:49 [binder, in Coq.rtauto.Rtauto]
d:498 [binder, in Coq.Lists.List]
D:5 [binder, in Coq.Reals.Rderiv]
d:5 [binder, in Coq.Init.Decimal]
d:5 [binder, in Coq.Numbers.DecimalFacts]
d:5 [binder, in Coq.Init.Hexadecimal]
d:5 [binder, in Coq.Numbers.HexadecimalNat]
d:5 [binder, in Coq.Numbers.DecimalN]
d:5 [binder, in Coq.Numbers.DecimalZ]
d:5 [binder, in Coq.Numbers.HexadecimalFacts]
d:5 [binder, in Coq.Numbers.HexadecimalZ]
d:5 [binder, in Coq.Numbers.HexadecimalN]
d:5 [binder, in Coq.Reals.PSeries_reg]
d:5 [binder, in Coq.QArith.Qround]
d:5 [binder, in Coq.Numbers.DecimalNat]
d:50 [binder, in Coq.Numbers.DecimalFacts]
d:50 [binder, in Coq.Init.Hexadecimal]
d:50 [binder, in Coq.Numbers.HexadecimalNat]
d:50 [binder, in Coq.Numbers.HexadecimalFacts]
D:50 [binder, in Coq.Reals.Rtopology]
d:50 [binder, in Coq.Numbers.DecimalNat]
d:51 [binder, in Coq.Init.Decimal]
d:51 [binder, in Coq.Numbers.NatInt.NZPow]
d:51 [binder, in Coq.Numbers.HexadecimalFacts]
D:51 [binder, in Coq.Reals.Rtopology]
d:51 [binder, in Coq.QArith.QArith_base]
D:52 [binder, in Coq.Reals.Rderiv]
d:52 [binder, in Coq.Numbers.DecimalFacts]
D:52 [binder, in Coq.Reals.Rlimit]
d:52 [binder, in Coq.micromega.Refl]
d:527 [binder, in Coq.Lists.List]
d:53 [binder, in Coq.Numbers.DecimalFacts]
d:53 [binder, in Coq.Numbers.HexadecimalPos]
d:53 [binder, in Coq.Init.Hexadecimal]
d:53 [binder, in Coq.Numbers.DecimalPos]
d:54 [binder, in Coq.Reals.R_sqrt]
d:54 [binder, in Coq.Init.Hexadecimal]
d:55 [binder, in Coq.Reals.Ranalysis2]
d:55 [binder, in Coq.Numbers.HexadecimalPos]
d:55 [binder, in Coq.Numbers.NatInt.NZPow]
d:55 [binder, in Coq.Numbers.DecimalPos]
d:55 [binder, in Coq.ZArith.Znumtheory]
d:56 [binder, in Coq.Reals.Runcountable]
d:56 [binder, in Coq.Init.Decimal]
d:56 [binder, in Coq.Numbers.HexadecimalPos]
d:56 [binder, in Coq.Numbers.HexadecimalFacts]
D:56 [binder, in Coq.Reals.Rlimit]
d:56 [binder, in Coq.Numbers.DecimalPos]
D:57 [binder, in Coq.Reals.Rderiv]
d:57 [binder, in Coq.Numbers.DecimalFacts]
d:57 [binder, in Coq.Numbers.HexadecimalFacts]
d:58 [binder, in Coq.Numbers.HexadecimalPos]
d:58 [binder, in Coq.Numbers.HexadecimalFacts]
d:58 [binder, in Coq.Numbers.DecimalPos]
d:582 [binder, in Coq.ssr.ssrbool]
d:589 [binder, in Coq.Lists.List]
d:59 [binder, in Coq.Reals.Ranalysis2]
d:59 [binder, in Coq.Init.Decimal]
d:59 [binder, in Coq.Numbers.DecimalFacts]
d:59 [binder, in Coq.FSets.FMapAVL]
d:59 [binder, in Coq.Numbers.HexadecimalFacts]
D:59 [binder, in Coq.Reals.Rlimit]
d:59 [binder, in Coq.micromega.ZMicromega]
d:6 [binder, in Coq.Init.Decimal]
d:6 [binder, in Coq.Numbers.DecimalFacts]
d:6 [binder, in Coq.Numbers.DecimalString]
d:6 [binder, in Coq.Numbers.HexadecimalPos]
d:6 [binder, in Coq.Numbers.DecimalQ]
d:6 [binder, in Coq.Init.Hexadecimal]
d:6 [binder, in Coq.Numbers.HexadecimalFacts]
d:6 [binder, in Coq.Numbers.HexadecimalString]
d:6 [binder, in Coq.Numbers.DecimalPos]
d:60 [binder, in Coq.Numbers.DecimalFacts]
d:60 [binder, in Coq.Numbers.DecimalQ]
d:60 [binder, in Coq.Numbers.HexadecimalFacts]
d:600 [binder, in Coq.MSets.MSetRBT]
D:61 [binder, in Coq.Reals.Rderiv]
d:61 [binder, in Coq.Init.Decimal]
d:61 [binder, in Coq.Numbers.DecimalFacts]
d:61 [binder, in Coq.FSets.FMapFullAVL]
d:61 [binder, in Coq.ZArith.Znumtheory]
d:62 [binder, in Coq.Numbers.DecimalQ]
d:62 [binder, in Coq.Numbers.HexadecimalFacts]
d:63 [binder, in Coq.Init.Decimal]
d:63 [binder, in Coq.Numbers.DecimalFacts]
d:63 [binder, in Coq.Numbers.HexadecimalPos]
d:63 [binder, in Coq.Numbers.DecimalQ]
d:63 [binder, in Coq.setoid_ring.Field_theory]
d:63 [binder, in Coq.Init.Nat]
d:64 [binder, in Coq.Reals.Runcountable]
d:64 [binder, in Coq.Numbers.DecimalFacts]
d:64 [binder, in Coq.Numbers.HexadecimalPos]
d:64 [binder, in Coq.Numbers.HexadecimalFacts]
D:64 [binder, in Coq.Reals.Rlimit]
d:64 [binder, in Coq.Numbers.DecimalPos]
d:64 [binder, in Coq.ZArith.Znumtheory]
d:641 [binder, in Coq.ssr.ssrbool]
d:646 [binder, in Coq.ssr.ssrbool]
d:65 [binder, in Coq.Numbers.HexadecimalPos]
d:65 [binder, in Coq.FSets.FMapFullAVL]
d:654 [binder, in Coq.ssr.ssrbool]
d:66 [binder, in Coq.Init.Decimal]
d:66 [binder, in Coq.Numbers.HexadecimalPos]
d:660 [binder, in Coq.ssr.ssrbool]
d:67 [binder, in Coq.Init.Decimal]
d:67 [binder, in Coq.setoid_ring.Field_theory]
d:67 [binder, in Coq.Init.Nat]
d:67 [binder, in Coq.ZArith.Zpower]
d:67 [binder, in Coq.Numbers.HexadecimalQ]
d:67 [binder, in Coq.micromega.RMicromega]
d:67 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
d:68 [binder, in Coq.Numbers.HexadecimalPos]
d:68 [binder, in Coq.Init.Nat]
d:68 [binder, in Coq.Numbers.DecimalPos]
d:685 [binder, in Coq.MSets.MSetRBT]
d:687 [binder, in Coq.MSets.MSetRBT]
D:69 [binder, in Coq.Reals.Rpower]
D:69 [binder, in Coq.Reals.Rtopology]
d:69 [binder, in Coq.Numbers.HexadecimalQ]
d:69 [binder, in Coq.micromega.RMicromega]
d:69 [binder, in Coq.ZArith.Znumtheory]
d:7 [binder, in Coq.Numbers.DecimalFacts]
d:7 [binder, in Coq.Numbers.DecimalN]
d:7 [binder, in Coq.Numbers.DecimalZ]
d:7 [binder, in Coq.Numbers.HexadecimalFacts]
d:7 [binder, in Coq.Numbers.HexadecimalZ]
d:7 [binder, in Coq.Numbers.HexadecimalN]
d:70 [binder, in Coq.ZArith.BinIntDef]
d:70 [binder, in Coq.ZArith.Zpower]
D:70 [binder, in Coq.Reals.Rlimit]
d:70 [binder, in Coq.Numbers.HexadecimalQ]
d:70 [binder, in Coq.Numbers.DecimalPos]
d:71 [binder, in Coq.ZArith.BinIntDef]
d:71 [binder, in Coq.micromega.RMicromega]
d:71 [binder, in Coq.Numbers.DecimalPos]
d:72 [binder, in Coq.ZArith.BinIntDef]
d:72 [binder, in Coq.Numbers.HexadecimalPos]
d:72 [binder, in Coq.Init.Nat]
D:72 [binder, in Coq.Reals.Rtopology]
d:72 [binder, in Coq.Numbers.HexadecimalQ]
d:72 [binder, in Coq.ZArith.Znumtheory]
d:72 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
D:73 [binder, in Coq.Reals.Rderiv]
d:73 [binder, in Coq.Numbers.DecimalFacts]
d:73 [binder, in Coq.Init.Nat]
d:74 [binder, in Coq.Numbers.DecimalFacts]
d:74 [binder, in Coq.ZArith.BinIntDef]
d:74 [binder, in Coq.Numbers.HexadecimalPos]
d:74 [binder, in Coq.setoid_ring.Field_theory]
D:74 [binder, in Coq.Reals.Rpower]
D:74 [binder, in Coq.Reals.Rtopology]
d:75 [binder, in Coq.Numbers.DecimalFacts]
d:75 [binder, in Coq.Numbers.HexadecimalPos]
d:75 [binder, in Coq.ZArith.Znumtheory]
d:76 [binder, in Coq.Numbers.DecimalFacts]
d:76 [binder, in Coq.ZArith.BinIntDef]
D:76 [binder, in Coq.Reals.Rlimit]
d:78 [binder, in Coq.ZArith.BinIntDef]
d:8 [binder, in Coq.Reals.Rderiv]
d:8 [binder, in Coq.Numbers.DecimalFacts]
d:8 [binder, in Coq.Numbers.DecimalString]
d:8 [binder, in Coq.Numbers.HexadecimalPos]
d:8 [binder, in Coq.Numbers.DecimalQ]
d:8 [binder, in Coq.Numbers.DecimalN]
d:8 [binder, in Coq.Numbers.DecimalZ]
d:8 [binder, in Coq.Numbers.HexadecimalString]
d:8 [binder, in Coq.Numbers.HexadecimalZ]
d:8 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
d:8 [binder, in Coq.Numbers.HexadecimalN]
d:8 [binder, in Coq.Numbers.HexadecimalQ]
d:8 [binder, in Coq.Numbers.DecimalPos]
d:81 [binder, in Coq.setoid_ring.Field_theory]
D:84 [binder, in Coq.Reals.Rlimit]
d:84 [binder, in Coq.ZArith.Znumtheory]
d:846 [binder, in Coq.Lists.List]
d:85 [binder, in Coq.setoid_ring.Field_theory]
d:86 [binder, in Coq.Numbers.DecimalFacts]
d:87 [binder, in Coq.Numbers.DecimalFacts]
d:87 [binder, in Coq.Init.Nat]
d:870 [binder, in Coq.Lists.List]
d:88 [binder, in Coq.Init.Nat]
D:88 [binder, in Coq.Reals.Rtopology]
d:89 [binder, in Coq.Numbers.DecimalFacts]
d:89 [binder, in Coq.Init.Nat]
d:895 [binder, in Coq.Lists.List]
D:9 [binder, in Coq.Reals.Rderiv]
d:9 [binder, in Coq.Numbers.DecimalFacts]
d:9 [binder, in Coq.Numbers.HexadecimalPos]
d:9 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
d:9 [binder, in Coq.Numbers.HexadecimalQ]
d:9 [binder, in Coq.Numbers.DecimalPos]
d:9 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
D:90 [binder, in Coq.Reals.Rlimit]
d:91 [binder, in Coq.Numbers.DecimalFacts]
d:91 [binder, in Coq.setoid_ring.Field_theory]
d:91 [binder, in Coq.ZArith.Znumtheory]
d:915 [binder, in Coq.Lists.List]
D:92 [binder, in Coq.Reals.Rtopology]
D:93 [binder, in Coq.Reals.Rderiv]
d:94 [binder, in Coq.ZArith.Znumtheory]
d:95 [binder, in Coq.setoid_ring.Field_theory]
D:95 [binder, in Coq.Reals.Rlimit]
D:96 [binder, in Coq.Reals.Rtopology]
D:98 [binder, in Coq.Reals.Rtopology]
d:98 [binder, in Coq.ZArith.Znumtheory]

---

Global Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(68863 entries)

Notation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(985 entries)

Binder Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(44709 entries)

Module Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(761 entries)

Variable Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1497 entries)

Library Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(570 entries)

Lemma Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(11380 entries)

Constructor Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(976 entries)

Axiom Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(603 entries)

Inductive Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(298 entries)

Projection Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(460 entries)

Section Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(476 entries)

Instance Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(811 entries)

Abbreviation Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(1157 entries)

Definition Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(4018 entries)

Record Index

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(162 entries)