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

(72679 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

(1040 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

(47172 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

(791 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

(1553 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

(585 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

(11862 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

(1030 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

(625 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

(308 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

(474 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

(493 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

(896 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

(1443 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

(4242 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

(165 entries)

---

Q

Q [module, in Coq.QArith.Qminmax]
Q [record, in Coq.QArith.QArith_base]
Qabs [definition, in Coq.QArith.Qabs]
Qabs [library]
Qabs_Qgt_condition [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
Qabs_Rabs [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
Qabs_involutive [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
Qabs_gt [lemma, in Coq.QArith.Qabs]
Qabs_ge [lemma, in Coq.QArith.Qabs]
Qabs_diff_Qlt_condition [lemma, in Coq.QArith.Qabs]
Qabs_diff_Qle_condition [lemma, in Coq.QArith.Qabs]
Qabs_Qlt_condition [lemma, in Coq.QArith.Qabs]
Qabs_Qle_condition [lemma, in Coq.QArith.Qabs]
Qabs_triangle_reverse [lemma, in Coq.QArith.Qabs]
Qabs_Qminus [lemma, in Coq.QArith.Qabs]
Qabs_Qinv [lemma, in Coq.QArith.Qabs]
Qabs_Qmult [lemma, in Coq.QArith.Qabs]
Qabs_triangle [lemma, in Coq.QArith.Qabs]
Qabs_opp [lemma, in Coq.QArith.Qabs]
Qabs_nonneg [lemma, in Coq.QArith.Qabs]
Qabs_neg [lemma, in Coq.QArith.Qabs]
Qabs_pos [lemma, in Coq.QArith.Qabs]
Qabs_case [lemma, in Coq.QArith.Qabs]
Qarchimedean [lemma, in Coq.QArith.QArith_base]
QarchimedeanAbsExp2_Z [definition, in Coq.Reals.Cauchy.QExtra]
QarchimedeanExp2_Z [definition, in Coq.Reals.Cauchy.QExtra]
QarchimedeanLowAbsExp2_Z [definition, in Coq.Reals.Cauchy.QExtra]
QarchimedeanLowExp2_Z [definition, in Coq.Reals.Cauchy.QExtra]
Qarchimedean_power2_pos [lemma, in Coq.QArith.Qpower]
QArith [library]
QArith_base [library]
QBound [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
Qbound_ltabs_ZExp2_spec [lemma, in Coq.Reals.Cauchy.QExtra]
Qbound_ltabs_ZExp2 [definition, in Coq.Reals.Cauchy.QExtra]
Qbound_lt_ZExp2_spec [lemma, in Coq.Reals.Cauchy.QExtra]
Qbound_lt_ZExp2_test_4 [lemma, in Coq.Reals.Cauchy.QExtra]
Qbound_lt_ZExp2_test_3 [lemma, in Coq.Reals.Cauchy.QExtra]
Qbound_lt_ZExp2_test_2 [lemma, in Coq.Reals.Cauchy.QExtra]
Qbound_lt_ZExp2_test_1 [lemma, in Coq.Reals.Cauchy.QExtra]
Qbound_lt_ZExp2 [definition, in Coq.Reals.Cauchy.QExtra]
Qbound_leabs_ZExp2_spec [lemma, in Coq.Reals.Cauchy.QExtra]
Qbound_leabs_ZExp2 [definition, in Coq.Reals.Cauchy.QExtra]
Qbound_le_ZExp2_spec [lemma, in Coq.Reals.Cauchy.QExtra]
Qbound_le_ZExp2 [definition, in Coq.Reals.Cauchy.QExtra]
Qc [record, in Coq.QArith.Qcanon]
Qcabs [definition, in Coq.QArith.Qcabs]
Qcabs [library]
Qcabs_null [lemma, in Coq.QArith.Qcabs]
Qcabs_diff_Qcle_condition [lemma, in Coq.QArith.Qcabs]
Qcabs_Qcle_condition [lemma, in Coq.QArith.Qcabs]
Qcabs_triangle_reverse [lemma, in Coq.QArith.Qcabs]
Qcabs_Qcminus [lemma, in Coq.QArith.Qcabs]
Qcabs_Qcmult [lemma, in Coq.QArith.Qcabs]
Qcabs_triangle [lemma, in Coq.QArith.Qcabs]
Qcabs_opp [lemma, in Coq.QArith.Qcabs]
Qcabs_nonneg [lemma, in Coq.QArith.Qcabs]
Qcabs_neg [lemma, in Coq.QArith.Qcabs]
Qcabs_pos [lemma, in Coq.QArith.Qcabs]
Qcabs_case [lemma, in Coq.QArith.Qcabs]
Qcabs_canon [lemma, in Coq.QArith.Qcabs]
Qcanon [library]
QCauchySeq [definition, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
QCauchySeqLin [definition, in Coq.Reals.Cauchy.ConstructiveRcomplete]
Qccompare [definition, in Coq.QArith.Qcanon]
Qcdiv [definition, in Coq.QArith.Qcanon]
Qcdiv_mult_l [lemma, in Coq.QArith.Qcanon]
Qceiling [definition, in Coq.QArith.Qround]
Qceiling_resp_le [lemma, in Coq.QArith.Qround]
Qceiling_lt [lemma, in Coq.QArith.Qround]
Qceiling_Z [lemma, in Coq.QArith.Qround]
Qceq_alt [lemma, in Coq.QArith.Qcanon]
Qcft [definition, in Coq.QArith.Qcanon]
Qcge [abbreviation, in Coq.QArith.Qcanon]
Qcge_alt [lemma, in Coq.QArith.Qcanon]
Qcgt [abbreviation, in Coq.QArith.Qcanon]
Qcgt_alt [lemma, in Coq.QArith.Qcanon]
Qcinv [definition, in Coq.QArith.Qcanon]
Qcinv_mult_distr [lemma, in Coq.QArith.Qcanon]
Qcle [definition, in Coq.QArith.Qcanon]
Qcle_minus_iff [lemma, in Coq.QArith.Qcanon]
Qcle_lt_or_eq [lemma, in Coq.QArith.Qcanon]
Qcle_not_lt [lemma, in Coq.QArith.Qcanon]
Qcle_lt_trans [lemma, in Coq.QArith.Qcanon]
Qcle_trans [lemma, in Coq.QArith.Qcanon]
Qcle_antisym [lemma, in Coq.QArith.Qcanon]
Qcle_refl [lemma, in Coq.QArith.Qcanon]
Qcle_alt [lemma, in Coq.QArith.Qcanon]
Qcle_Qcabs [lemma, in Coq.QArith.Qcabs]
Qclt [definition, in Coq.QArith.Qcanon]
Qclt_minus_iff [lemma, in Coq.QArith.Qcanon]
Qclt_le_dec [lemma, in Coq.QArith.Qcanon]
Qclt_not_le [lemma, in Coq.QArith.Qcanon]
Qclt_trans [lemma, in Coq.QArith.Qcanon]
Qclt_le_trans [lemma, in Coq.QArith.Qcanon]
Qclt_le_weak [lemma, in Coq.QArith.Qcanon]
Qclt_not_eq [lemma, in Coq.QArith.Qcanon]
Qclt_alt [lemma, in Coq.QArith.Qcanon]
Qcmake [constructor, in Coq.QArith.Qcanon]
Qcminus [definition, in Coq.QArith.Qcanon]
Qcmult [definition, in Coq.QArith.Qcanon]
Qcmult_lt_compat_r [lemma, in Coq.QArith.Qcanon]
Qcmult_lt_0_le_reg_r [lemma, in Coq.QArith.Qcanon]
Qcmult_le_compat_r [lemma, in Coq.QArith.Qcanon]
Qcmult_div_r [lemma, in Coq.QArith.Qcanon]
Qcmult_inv_l [lemma, in Coq.QArith.Qcanon]
Qcmult_inv_r [lemma, in Coq.QArith.Qcanon]
Qcmult_integral_l [lemma, in Coq.QArith.Qcanon]
Qcmult_integral [lemma, in Coq.QArith.Qcanon]
Qcmult_plus_distr_l [lemma, in Coq.QArith.Qcanon]
Qcmult_plus_distr_r [lemma, in Coq.QArith.Qcanon]
Qcmult_comm [lemma, in Coq.QArith.Qcanon]
Qcmult_1_r [lemma, in Coq.QArith.Qcanon]
Qcmult_1_l [lemma, in Coq.QArith.Qcanon]
Qcmult_0_r [lemma, in Coq.QArith.Qcanon]
Qcmult_0_l [lemma, in Coq.QArith.Qcanon]
Qcmult_assoc [lemma, in Coq.QArith.Qcanon]
Qcnot_le_lt [lemma, in Coq.QArith.Qcanon]
Qcnot_lt_le [lemma, in Coq.QArith.Qcanon]
Qcompare [definition, in Coq.QArith.QArith_base]
Qcompare_comp [instance, in Coq.QArith.QArith_base]
Qcompare_spec [lemma, in Coq.QArith.QArith_base]
Qcompare_antisym [lemma, in Coq.QArith.QArith_base]
Qcopp [definition, in Coq.QArith.Qcanon]
Qcopp_le_compat [lemma, in Coq.QArith.Qcanon]
Qcopp_involutive [lemma, in Coq.QArith.Qcanon]
Qcplus [definition, in Coq.QArith.Qcanon]
Qcplus_le_compat [lemma, in Coq.QArith.Qcanon]
Qcplus_opp_r [lemma, in Coq.QArith.Qcanon]
Qcplus_comm [lemma, in Coq.QArith.Qcanon]
Qcplus_0_r [lemma, in Coq.QArith.Qcanon]
Qcplus_0_l [lemma, in Coq.QArith.Qcanon]
Qcplus_assoc [lemma, in Coq.QArith.Qcanon]
Qcpower [definition, in Coq.QArith.Qcanon]
Qcpower_pos [lemma, in Coq.QArith.Qcanon]
Qcpower_0 [lemma, in Coq.QArith.Qcanon]
Qcpower_1 [lemma, in Coq.QArith.Qcanon]
Qcri [instance, in Coq.nsatz.NsatzTactic]
Qcri [instance, in Coq.setoid_ring.Rings_Q]
Qcrt [definition, in Coq.QArith.Qcanon]
Qc_eq_bool_correct [lemma, in Coq.QArith.Qcanon]
Qc_eq_bool [definition, in Coq.QArith.Qcanon]
Qc_dec [lemma, in Coq.QArith.Qcanon]
Qc_eq_dec [lemma, in Coq.QArith.Qcanon]
Qc_decomp [lemma, in Coq.QArith.Qcanon]
Qc_is_canon [lemma, in Coq.QArith.Qcanon]
qdeduce [definition, in Coq.micromega.QMicromega]
QDen [abbreviation, in Coq.QArith.QArith_base]
Qden [projection, in Coq.QArith.QArith_base]
Qden_cancel [lemma, in Coq.QArith.QArith_base]
Qdi [instance, in Coq.nsatz.NsatzTactic]
Qdi [instance, in Coq.setoid_ring.Rings_Q]
Qdiv [definition, in Coq.QArith.QArith_base]
Qdiv_power [lemma, in Coq.QArith.Qpower]
Qdiv_mult_l [lemma, in Coq.QArith.QArith_base]
Qdiv_comp [instance, in Coq.QArith.QArith_base]
Qeq [definition, in Coq.QArith.QArith_base]
Qeqb_comp [instance, in Coq.QArith.QArith_base]
Qeq_eqR [lemma, in Coq.QArith.Qreals]
Qeq_false [lemma, in Coq.micromega.RMicromega]
Qeq_true [lemma, in Coq.micromega.RMicromega]
Qeq_bool_trans [lemma, in Coq.QArith.QArith_base]
Qeq_bool_sym [lemma, in Coq.QArith.QArith_base]
Qeq_bool_refl [lemma, in Coq.QArith.QArith_base]
Qeq_bool_comm [lemma, in Coq.QArith.QArith_base]
Qeq_bool_neq [lemma, in Coq.QArith.QArith_base]
Qeq_eq_bool [lemma, in Coq.QArith.QArith_base]
Qeq_bool_eq [lemma, in Coq.QArith.QArith_base]
Qeq_bool_iff [lemma, in Coq.QArith.QArith_base]
Qeq_bool [definition, in Coq.QArith.QArith_base]
Qeq_dec [lemma, in Coq.QArith.QArith_base]
Qeq_trans [lemma, in Coq.QArith.QArith_base]
Qeq_sym [lemma, in Coq.QArith.QArith_base]
Qeq_refl [lemma, in Coq.QArith.QArith_base]
Qeq_alt [lemma, in Coq.QArith.QArith_base]
Qeval_nformula_dec [lemma, in Coq.micromega.QMicromega]
Qeval_op1 [definition, in Coq.micromega.QMicromega]
Qeval_nformula [definition, in Coq.micromega.QMicromega]
Qeval_formula_compat [lemma, in Coq.micromega.QMicromega]
Qeval_formula' [definition, in Coq.micromega.QMicromega]
Qeval_formula [definition, in Coq.micromega.QMicromega]
Qeval_op2_hold [lemma, in Coq.micromega.QMicromega]
Qeval_op2 [definition, in Coq.micromega.QMicromega]
Qeval_bop2 [definition, in Coq.micromega.QMicromega]
Qeval_pop2 [definition, in Coq.micromega.QMicromega]
Qeval_expr_compat [lemma, in Coq.micromega.QMicromega]
Qeval_expr' [definition, in Coq.micromega.QMicromega]
Qeval_expr_simpl [lemma, in Coq.micromega.QMicromega]
Qeval_expr [definition, in Coq.micromega.QMicromega]
Qeval_nformula [definition, in Coq.micromega.RMicromega]
QExtra [library]
qe:29 [binder, in Coq.nsatz.NsatzTactic]
qe:59 [binder, in Coq.nsatz.NsatzTactic]
Qfield [library]
Qfloor [definition, in Coq.QArith.Qround]
Qfloor_resp_le [lemma, in Coq.QArith.Qround]
Qfloor_le [lemma, in Coq.QArith.Qround]
Qfloor_Z [lemma, in Coq.QArith.Qround]
Qge [abbreviation, in Coq.QArith.QArith_base]
Qge_le [lemma, in Coq.QArith.QArith_base]
Qge_alt [lemma, in Coq.QArith.QArith_base]
Qgt [abbreviation, in Coq.QArith.QArith_base]
Qgt_lt [lemma, in Coq.QArith.QArith_base]
Qgt_alt [lemma, in Coq.QArith.QArith_base]
QHasMinMax [module, in Coq.QArith.Qminmax]
QHasMinMax.max [definition, in Coq.QArith.Qminmax]
QHasMinMax.max_r [definition, in Coq.QArith.Qminmax]
QHasMinMax.max_l [definition, in Coq.QArith.Qminmax]
QHasMinMax.min [definition, in Coq.QArith.Qminmax]
QHasMinMax.min_r [definition, in Coq.QArith.Qminmax]
QHasMinMax.min_l [definition, in Coq.QArith.Qminmax]
QHasMinMax.QMM [module, in Coq.QArith.Qminmax]
Qinv [definition, in Coq.QArith.QArith_base]
Qinv_power_n [lemma, in Coq.QArith.Qpower]
Qinv_power [lemma, in Coq.QArith.Qpower]
Qinv_power_positive [lemma, in Coq.QArith.Qpower]
Qinv_lt_contravar [lemma, in Coq.QArith.QArith_base]
Qinv_lt_0_compat [lemma, in Coq.QArith.QArith_base]
Qinv_le_0_compat [lemma, in Coq.QArith.QArith_base]
Qinv_minus_distr [lemma, in Coq.QArith.QArith_base]
Qinv_plus_distr [lemma, in Coq.QArith.QArith_base]
Qinv_neg [lemma, in Coq.QArith.QArith_base]
Qinv_pos [lemma, in Coq.QArith.QArith_base]
Qinv_mult_distr [lemma, in Coq.QArith.QArith_base]
Qinv_involutive [lemma, in Coq.QArith.QArith_base]
Qinv_comp [instance, in Coq.QArith.QArith_base]
Qle [definition, in Coq.QArith.QArith_base]
Qleb_comp [instance, in Coq.QArith.QArith_base]
Qle_trans_swap_hyp [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
Qle_Rle [lemma, in Coq.QArith.Qreals]
Qle_Qabs [lemma, in Coq.QArith.Qabs]
Qle_true [lemma, in Coq.micromega.RMicromega]
Qle_floor_ceiling [lemma, in Coq.QArith.Qround]
Qle_ceiling [lemma, in Coq.QArith.Qround]
Qle_shift_inv_r [lemma, in Coq.QArith.QArith_base]
Qle_shift_div_r [lemma, in Coq.QArith.QArith_base]
Qle_shift_inv_l [lemma, in Coq.QArith.QArith_base]
Qle_shift_div_l [lemma, in Coq.QArith.QArith_base]
Qle_minus_iff [lemma, in Coq.QArith.QArith_base]
Qle_lt_or_eq [lemma, in Coq.QArith.QArith_base]
Qle_not_lt [lemma, in Coq.QArith.QArith_base]
Qle_lt_trans [lemma, in Coq.QArith.QArith_base]
Qle_ge [lemma, in Coq.QArith.QArith_base]
Qle_lteq [lemma, in Coq.QArith.QArith_base]
Qle_trans [lemma, in Coq.QArith.QArith_base]
Qle_antisym [lemma, in Coq.QArith.QArith_base]
Qle_refl [lemma, in Coq.QArith.QArith_base]
Qle_comp [instance, in Coq.QArith.QArith_base]
Qle_bool_imp_le [lemma, in Coq.QArith.QArith_base]
Qle_bool_iff [lemma, in Coq.QArith.QArith_base]
Qle_bool [definition, in Coq.QArith.QArith_base]
Qle_alt [lemma, in Coq.QArith.QArith_base]
Qlowbound_ltabs_ZExp2_spec [lemma, in Coq.Reals.Cauchy.QExtra]
Qlowbound_lt_ZExp2_spec [lemma, in Coq.Reals.Cauchy.QExtra]
Qlowbound_ltabs_ZExp2_opp [lemma, in Coq.Reals.Cauchy.QExtra]
Qlowbound_ltabs_ZExp2_inv [lemma, in Coq.Reals.Cauchy.QExtra]
Qlowbound_ltabs_ZExp2 [definition, in Coq.Reals.Cauchy.QExtra]
Qlt [definition, in Coq.QArith.QArith_base]
Qlt_trans_swap_hyp [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
Qlt_Rlt [lemma, in Coq.QArith.Qreals]
Qlt_bool_iff [lemma, in Coq.micromega.QMicromega]
Qlt_bool [definition, in Coq.micromega.QMicromega]
Qlt_floor [lemma, in Coq.QArith.Qround]
Qlt_shift_inv_r [lemma, in Coq.QArith.QArith_base]
Qlt_shift_div_r [lemma, in Coq.QArith.QArith_base]
Qlt_shift_inv_l [lemma, in Coq.QArith.QArith_base]
Qlt_shift_div_l [lemma, in Coq.QArith.QArith_base]
Qlt_minus_iff [lemma, in Coq.QArith.QArith_base]
Qlt_le_dec [lemma, in Coq.QArith.QArith_base]
Qlt_not_le [lemma, in Coq.QArith.QArith_base]
Qlt_trans [lemma, in Coq.QArith.QArith_base]
Qlt_le_trans [lemma, in Coq.QArith.QArith_base]
Qlt_gt [lemma, in Coq.QArith.QArith_base]
Qlt_le_weak [lemma, in Coq.QArith.QArith_base]
Qlt_leneq [lemma, in Coq.QArith.QArith_base]
Qlt_not_eq [lemma, in Coq.QArith.QArith_base]
Qlt_irrefl [lemma, in Coq.QArith.QArith_base]
Qlt_compat [instance, in Coq.QArith.QArith_base]
Qlt_alt [lemma, in Coq.QArith.QArith_base]
Qmake [constructor, in Coq.QArith.QArith_base]
Qmake_Qdiv [lemma, in Coq.QArith.QArith_base]
Qmax [definition, in Coq.QArith.Qminmax]
QMicromega [library]
Qmin [definition, in Coq.QArith.Qminmax]
Qminmax [library]
Qminus [definition, in Coq.QArith.QArith_base]
Qminus_comp [instance, in Coq.QArith.QArith_base]
Qminus' [definition, in Coq.QArith.Qreduction]
Qminus'_correct [lemma, in Coq.QArith.Qreduction]
Qmult [definition, in Coq.QArith.QArith_base]
Qmult_integral [lemma, in Coq.micromega.RMicromega]
Qmult_power [lemma, in Coq.QArith.Qpower]
Qmult_power_positive [lemma, in Coq.QArith.Qpower]
Qmult_le_compat_nonneg [lemma, in Coq.QArith.QArith_base]
Qmult_le_lt_compat_pos [lemma, in Coq.QArith.QArith_base]
Qmult_lt_compat_nonneg [lemma, in Coq.QArith.QArith_base]
Qmult_lt_1_compat [lemma, in Coq.QArith.QArith_base]
Qmult_le_1_compat [lemma, in Coq.QArith.QArith_base]
Qmult_lt_0_compat [lemma, in Coq.QArith.QArith_base]
Qmult_le_0_compat [lemma, in Coq.QArith.QArith_base]
Qmult_lt_l [lemma, in Coq.QArith.QArith_base]
Qmult_lt_r [lemma, in Coq.QArith.QArith_base]
Qmult_lt_compat_r [lemma, in Coq.QArith.QArith_base]
Qmult_le_l [lemma, in Coq.QArith.QArith_base]
Qmult_le_r [lemma, in Coq.QArith.QArith_base]
Qmult_lt_0_le_reg_r [lemma, in Coq.QArith.QArith_base]
Qmult_le_compat_r [lemma, in Coq.QArith.QArith_base]
Qmult_frac_r [lemma, in Coq.QArith.QArith_base]
Qmult_frac_l [lemma, in Coq.QArith.QArith_base]
Qmult_inject_Z_r [lemma, in Coq.QArith.QArith_base]
Qmult_inject_Z_l [lemma, in Coq.QArith.QArith_base]
Qmult_inj_l [lemma, in Coq.QArith.QArith_base]
Qmult_inj_r [lemma, in Coq.QArith.QArith_base]
Qmult_div_r [lemma, in Coq.QArith.QArith_base]
Qmult_inv_r [lemma, in Coq.QArith.QArith_base]
Qmult_integral_l [lemma, in Coq.QArith.QArith_base]
Qmult_integral [lemma, in Coq.QArith.QArith_base]
Qmult_plus_distr_l [lemma, in Coq.QArith.QArith_base]
Qmult_plus_distr_r [lemma, in Coq.QArith.QArith_base]
Qmult_comm [lemma, in Coq.QArith.QArith_base]
Qmult_1_r [lemma, in Coq.QArith.QArith_base]
Qmult_1_l [lemma, in Coq.QArith.QArith_base]
Qmult_0_r [lemma, in Coq.QArith.QArith_base]
Qmult_0_l [lemma, in Coq.QArith.QArith_base]
Qmult_assoc [lemma, in Coq.QArith.QArith_base]
Qmult_comp [instance, in Coq.QArith.QArith_base]
Qmult' [definition, in Coq.QArith.Qreduction]
Qmult'_correct [lemma, in Coq.QArith.Qreduction]
Qnegate [definition, in Coq.micromega.QMicromega]
Qnormalise [definition, in Coq.micromega.QMicromega]
Qnot_lt_iff_le [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
Qnot_le_iff_lt [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
Qnot_le_lt [lemma, in Coq.QArith.QArith_base]
Qnot_lt_le [lemma, in Coq.QArith.QArith_base]
Qnot_eq_sym [lemma, in Coq.QArith.QArith_base]
QNpower [lemma, in Coq.micromega.QMicromega]
Qnum [projection, in Coq.QArith.QArith_base]
Qnum_cancel [lemma, in Coq.QArith.QArith_base]
qn:131 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
Qopp [definition, in Coq.QArith.QArith_base]
Qopp_mult_mone [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
Qopp_opp [lemma, in Coq.QArith.Qfield]
Qopp_plus [lemma, in Coq.QArith.Qfield]
Qopp_lt_compat [lemma, in Coq.QArith.QArith_base]
Qopp_le_compat [lemma, in Coq.QArith.QArith_base]
Qopp_involutive [lemma, in Coq.QArith.QArith_base]
Qopp_comp [instance, in Coq.QArith.QArith_base]
Qops [instance, in Coq.nsatz.NsatzTactic]
Qops [instance, in Coq.setoid_ring.Rings_Q]
QOrder [module, in Coq.QArith.QOrderedType]
QOrderedType [library]
Qplus [definition, in Coq.QArith.QArith_base]
Qplus_lt_compat [lemma, in Coq.QArith.QArith_base]
Qplus_lt_r [lemma, in Coq.QArith.QArith_base]
Qplus_lt_l [lemma, in Coq.QArith.QArith_base]
Qplus_le_r [lemma, in Coq.QArith.QArith_base]
Qplus_le_l [lemma, in Coq.QArith.QArith_base]
Qplus_lt_le_compat [lemma, in Coq.QArith.QArith_base]
Qplus_le_compat [lemma, in Coq.QArith.QArith_base]
Qplus_inj_l [lemma, in Coq.QArith.QArith_base]
Qplus_inj_r [lemma, in Coq.QArith.QArith_base]
Qplus_opp_r [lemma, in Coq.QArith.QArith_base]
Qplus_comm [lemma, in Coq.QArith.QArith_base]
Qplus_0_r [lemma, in Coq.QArith.QArith_base]
Qplus_0_l [lemma, in Coq.QArith.QArith_base]
Qplus_assoc [lemma, in Coq.QArith.QArith_base]
Qplus_comp [instance, in Coq.QArith.QArith_base]
Qplus' [definition, in Coq.QArith.Qreduction]
Qplus'_correct [lemma, in Coq.QArith.Qreduction]
qPos:332 [binder, in Coq.Reals.Abstract.ConstructiveReals]
Qpower [definition, in Coq.QArith.QArith_base]
Qpower [library]
Qpower_2powneg_le_inv [lemma, in Coq.Reals.Cauchy.ConstructiveRcomplete]
Qpower_theory [lemma, in Coq.QArith.Qfield]
Qpower_positive_zero [lemma, in Coq.micromega.RMicromega]
Qpower_positive_eq_zero [lemma, in Coq.micromega.RMicromega]
Qpower_le_compat_l_inv [lemma, in Coq.QArith.Qpower]
Qpower_lt_compat_l_inv [lemma, in Coq.QArith.Qpower]
Qpower_le_compat_l [lemma, in Coq.QArith.Qpower]
Qpower_lt_compat_l [lemma, in Coq.QArith.Qpower]
Qpower_decomp_neg_neg [lemma, in Coq.QArith.Qpower]
Qpower_decomp_neg_pos [lemma, in Coq.QArith.Qpower]
Qpower_decomp_pos [lemma, in Coq.QArith.Qpower]
Qpower_mult [lemma, in Coq.QArith.Qpower]
Qpower_minus_neg [lemma, in Coq.QArith.Qpower]
Qpower_minus_pos [lemma, in Coq.QArith.Qpower]
Qpower_minus [lemma, in Coq.QArith.Qpower]
Qpower_opp [lemma, in Coq.QArith.Qpower]
Qpower_plus' [lemma, in Coq.QArith.Qpower]
Qpower_plus [lemma, in Coq.QArith.Qpower]
Qpower_1_le [lemma, in Coq.QArith.Qpower]
Qpower_1_le_pos [lemma, in Coq.QArith.Qpower]
Qpower_1_lt [lemma, in Coq.QArith.Qpower]
Qpower_1_lt_pos [lemma, in Coq.QArith.Qpower]
Qpower_0_lt [lemma, in Coq.QArith.Qpower]
Qpower_pos [abbreviation, in Coq.QArith.Qpower]
Qpower_0_le [lemma, in Coq.QArith.Qpower]
Qpower_not_0 [lemma, in Coq.QArith.Qpower]
Qpower_1_r [lemma, in Coq.QArith.Qpower]
Qpower_0_r [lemma, in Coq.QArith.Qpower]
Qpower_1 [lemma, in Coq.QArith.Qpower]
Qpower_0 [lemma, in Coq.QArith.Qpower]
Qpower_decomp [abbreviation, in Coq.QArith.Qpower]
Qpower_decomp_positive [lemma, in Coq.QArith.Qpower]
Qpower_mult_positive [lemma, in Coq.QArith.Qpower]
Qpower_minus_positive [lemma, in Coq.QArith.Qpower]
Qpower_plus_positive [lemma, in Coq.QArith.Qpower]
Qpower_pos_positive [lemma, in Coq.QArith.Qpower]
Qpower_not_0_positive [lemma, in Coq.QArith.Qpower]
Qpower_positive_0 [lemma, in Coq.QArith.Qpower]
Qpower_positive_1 [lemma, in Coq.QArith.Qpower]
Qpower_2_neg_le_one [lemma, in Coq.Reals.ClassicalDedekindReals]
Qpower_2_invneg_le_pow [lemma, in Coq.Reals.ClassicalDedekindReals]
Qpower_2_neg_eq_natpow_inv [lemma, in Coq.Reals.ClassicalDedekindReals]
Qpower_comp [instance, in Coq.QArith.QArith_base]
Qpower_positive_comp [instance, in Coq.QArith.QArith_base]
Qpower_positive [definition, in Coq.QArith.QArith_base]
Qpower0 [lemma, in Coq.micromega.RMicromega]
QP':114 [binder, in Coq.setoid_ring.Ring_polynom]
QP':116 [binder, in Coq.micromega.EnvRing]
QQ':111 [binder, in Coq.setoid_ring.Ring_polynom]
QQ':112 [binder, in Coq.setoid_ring.Ring_polynom]
QQ':113 [binder, in Coq.micromega.EnvRing]
QQ':114 [binder, in Coq.micromega.EnvRing]
qrd:61 [binder, in Coq.ZArith.Zpower]
Qreals [library]
Qred [definition, in Coq.QArith.Qreduction]
Qreduce_zero [lemma, in Coq.QArith.QArith_base]
Qreduce_den_inject_Z_r [lemma, in Coq.QArith.QArith_base]
Qreduce_den_inject_Z_l [lemma, in Coq.QArith.QArith_base]
Qreduce_den_r [lemma, in Coq.QArith.QArith_base]
Qreduce_den_l [lemma, in Coq.QArith.QArith_base]
Qreduce_num_r [lemma, in Coq.QArith.QArith_base]
Qreduce_num_l [lemma, in Coq.QArith.QArith_base]
Qreduce_r [lemma, in Coq.QArith.QArith_base]
Qreduce_l [lemma, in Coq.QArith.QArith_base]
Qreduction [library]
Qred_involutive [lemma, in Coq.QArith.Qcanon]
Qred_iff [lemma, in Coq.QArith.Qcanon]
Qred_identity2 [lemma, in Coq.QArith.Qcanon]
Qred_identity [lemma, in Coq.QArith.Qcanon]
Qred_abs [lemma, in Coq.QArith.Qcabs]
Qred_lt [lemma, in Coq.QArith.Qreduction]
Qred_le [lemma, in Coq.QArith.Qreduction]
Qred_compare [lemma, in Coq.QArith.Qreduction]
Qred_opp [lemma, in Coq.QArith.Qreduction]
Qred_eq_iff [lemma, in Coq.QArith.Qreduction]
Qred_complete [lemma, in Coq.QArith.Qreduction]
Qred_correct [lemma, in Coq.QArith.Qreduction]
QReval_formula_compat [lemma, in Coq.micromega.RMicromega]
QReval_formula' [definition, in Coq.micromega.RMicromega]
QReval_formula [definition, in Coq.micromega.RMicromega]
QReval_expr [definition, in Coq.micromega.RMicromega]
Qri [instance, in Coq.nsatz.NsatzTactic]
Qri [instance, in Coq.setoid_ring.Rings_Q]
Qring [library]
Qround [library]
qr:259 [binder, in Coq.ZArith.Zdiv]
qr:37 [binder, in Coq.ZArith.Zdiv]
qr:66 [binder, in Coq.ZArith.Zpower]
Qsft [definition, in Coq.QArith.Qfield]
Qsor [lemma, in Coq.micromega.QMicromega]
QSORaddon [lemma, in Coq.micromega.QMicromega]
QSORaddon [lemma, in Coq.micromega.RMicromega]
Qsqr_nonneg [lemma, in Coq.QArith.Qpower]
Qsrt [definition, in Coq.QArith.Qfield]
qs:74 [binder, in Coq.btauto.Algebra]
qs:88 [binder, in Coq.btauto.Algebra]
qs:93 [binder, in Coq.btauto.Algebra]
qs:97 [binder, in Coq.btauto.Algebra]
QTautoChecker [definition, in Coq.micromega.QMicromega]
QTautoChecker_sound [lemma, in Coq.micromega.QMicromega]
quadruple [lemma, in Coq.Reals.Ranalysis2]
quadruple_var [lemma, in Coq.Reals.Ranalysis2]
qualifE [lemma, in Coq.ssr.ssrbool]
Qualifier [constructor, in Coq.ssr.ssrbool]
qualifier [inductive, in Coq.ssr.ssrbool]
qunsat [definition, in Coq.micromega.QMicromega]
quotient [lemma, in Coq.Arith.Euclid]
quotient_by_2 [lemma, in Coq.Numbers.Cyclic.Int31.Cyclic31]
quotient_by_2 [abbreviation, in Coq.Numbers.Cyclic.Int63.Int63]
quotient_by_2 [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
QuotRem [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemNotation [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
_ rem _ [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
_ ÷ _ [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.quot_rem [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.quot_wd [instance, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.rem_opp_r [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.rem_opp_l [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.rem_bound_pos [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRemSpec.rem_wd [instance, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRem' [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRem.quot [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
QuotRem.rem [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
quots [definition, in Coq.micromega.ZifySint63]
quotsSpec [instance, in Coq.micromega.ZifySint63]
quots_spec [lemma, in Coq.micromega.ZifySint63]
quo:123 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
quo:137 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
quo:162 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]
quo:178 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]
quo:398 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]
QWeakChecker [definition, in Coq.micromega.QMicromega]
QWeakChecker_sound [lemma, in Coq.micromega.QMicromega]
QWitness [definition, in Coq.micromega.QMicromega]
Q_as_OT.compare_spec [definition, in Coq.QArith.QOrderedType]
Q_as_OT.le_lteq [definition, in Coq.QArith.QOrderedType]
Q_as_OT.lt_compat [instance, in Coq.QArith.QOrderedType]
Q_as_OT.lt_strorder [instance, in Coq.QArith.QOrderedType]
Q_as_OT.compare [definition, in Coq.QArith.QOrderedType]
Q_as_OT.le [definition, in Coq.QArith.QOrderedType]
Q_as_OT.lt [definition, in Coq.QArith.QOrderedType]
Q_as_OT [module, in Coq.QArith.QOrderedType]
Q_as_DT.eqb_eq [definition, in Coq.QArith.QOrderedType]
Q_as_DT.eqb [definition, in Coq.QArith.QOrderedType]
Q_as_DT.eq_equiv [definition, in Coq.QArith.QOrderedType]
Q_as_DT.eq [definition, in Coq.QArith.QOrderedType]
Q_as_DT.t [definition, in Coq.QArith.QOrderedType]
Q_as_DT [module, in Coq.QArith.QOrderedType]
Q_apart_0_1 [lemma, in Coq.QArith.Qcanon]
Q_one_zero [lemma, in Coq.nsatz.NsatzTactic]
Q_one_zero [lemma, in Coq.setoid_ring.Rings_Q]
Q_hprop:1038 [binder, in Coq.Init.Specif]
Q_hprop:914 [binder, in Coq.Init.Specif]
Q_hprop:776 [binder, in Coq.Init.Specif]
Q_hprop:652 [binder, in Coq.Init.Specif]
Q_of_RcstR [lemma, in Coq.micromega.RMicromega]
Q_of_Rcst [definition, in Coq.micromega.RMicromega]
Q_hprop:937 [binder, in Coq.Init.Logic]
Q_hprop:803 [binder, in Coq.Init.Logic]
Q_hprop:782 [binder, in Coq.Init.Logic]
Q_hprop:770 [binder, in Coq.Init.Logic]
Q_dec [lemma, in Coq.QArith.QArith_base]
Q_apart_0_1 [lemma, in Coq.QArith.QArith_base]
Q_Setoid [instance, in Coq.QArith.QArith_base]
q':10 [binder, in Coq.QArith.Qcanon]
q':10 [binder, in Coq.QArith.Qreduction]
q':125 [binder, in Coq.PArith.BinPos]
q':14 [binder, in Coq.QArith.Qcanon]
q':152 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]
q':216 [binder, in Coq.Init.Specif]
q':226 [binder, in Coq.Init.Specif]
q':27 [binder, in Coq.QArith.Qreduction]
q':29 [binder, in Coq.QArith.Qreduction]
q':31 [binder, in Coq.Numbers.HexadecimalR]
q':31 [binder, in Coq.Numbers.DecimalR]
q':45 [binder, in Coq.Numbers.DecimalQ]
q':45 [binder, in Coq.Numbers.HexadecimalQ]
q':79 [binder, in Coq.Arith.PeanoNat]
q':8 [binder, in Coq.QArith.Qcanon]
Q.plus_min_distr_r [lemma, in Coq.QArith.Qminmax]
Q.plus_min_distr_l [lemma, in Coq.QArith.Qminmax]
Q.plus_max_distr_r [lemma, in Coq.QArith.Qminmax]
Q.plus_max_distr_l [lemma, in Coq.QArith.Qminmax]
q0:150 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:152 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:158 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:160 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:162 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:164 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:170 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:172 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:174 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:176 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:177 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:178 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:180 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q0:182 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q1:10 [binder, in Coq.Numbers.NatInt.NZDiv]
q1:101 [binder, in Coq.micromega.ZifyClasses]
q1:105 [binder, in Coq.micromega.ZifyClasses]
q1:12 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q1:14 [binder, in Coq.Numbers.NatInt.NZDiv]
Q1:158 [binder, in Coq.micromega.EnvRing]
Q1:165 [binder, in Coq.setoid_ring.Ring_polynom]
q1:18 [binder, in Coq.Numbers.NatInt.NZDiv]
q1:2 [binder, in Coq.QArith.Qreduction]
q1:34 [binder, in Coq.micromega.QMicromega]
q1:37 [binder, in Coq.micromega.QMicromega]
q1:39 [binder, in Coq.micromega.ZMicromega]
q1:41 [binder, in Coq.ZArith.Zdiv]
q1:43 [binder, in Coq.micromega.QMicromega]
q1:45 [binder, in Coq.micromega.ZMicromega]
q1:46 [binder, in Coq.ZArith.Zdiv]
q1:53 [binder, in Coq.setoid_ring.Field_theory]
q1:54 [binder, in Coq.micromega.ZifyClasses]
q1:6 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
q1:6 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
q1:60 [binder, in Coq.micromega.ZifyClasses]
q1:7 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
q1:83 [binder, in Coq.micromega.RMicromega]
Q2Qc [definition, in Coq.QArith.Qcanon]
Q2Qc_eq_iff [lemma, in Coq.QArith.Qcanon]
Q2R [definition, in Coq.Reals.Rdefinitions]
Q2RpowerRZ [lemma, in Coq.micromega.RMicromega]
Q2R_div [lemma, in Coq.QArith.Qreals]
Q2R_inv [lemma, in Coq.QArith.Qreals]
Q2R_minus [lemma, in Coq.QArith.Qreals]
Q2R_opp [lemma, in Coq.QArith.Qreals]
Q2R_mult [lemma, in Coq.QArith.Qreals]
Q2R_plus [lemma, in Coq.QArith.Qreals]
Q2R_pow_N [lemma, in Coq.micromega.RMicromega]
Q2R_pow_pos [lemma, in Coq.micromega.RMicromega]
Q2R_inv_ext [lemma, in Coq.micromega.RMicromega]
Q2R_1 [lemma, in Coq.micromega.RMicromega]
Q2R_0 [lemma, in Coq.micromega.RMicromega]
q2:102 [binder, in Coq.micromega.ZifyClasses]
q2:11 [binder, in Coq.Numbers.NatInt.NZDiv]
Q2:122 [binder, in Coq.micromega.EnvRing]
q2:13 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q2:15 [binder, in Coq.Numbers.NatInt.NZDiv]
q2:19 [binder, in Coq.Numbers.NatInt.NZDiv]
q2:3 [binder, in Coq.QArith.Qreduction]
q2:35 [binder, in Coq.micromega.QMicromega]
q2:38 [binder, in Coq.micromega.QMicromega]
q2:40 [binder, in Coq.micromega.ZMicromega]
q2:42 [binder, in Coq.ZArith.Zdiv]
q2:44 [binder, in Coq.micromega.QMicromega]
q2:46 [binder, in Coq.micromega.ZMicromega]
q2:47 [binder, in Coq.ZArith.Zdiv]
q2:54 [binder, in Coq.setoid_ring.Field_theory]
q2:55 [binder, in Coq.micromega.ZifyClasses]
q2:7 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
q2:7 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
q2:8 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
q2:84 [binder, in Coq.micromega.RMicromega]
q:1 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
q:1 [binder, in Coq.QArith.Qreduction]
q:10 [binder, in Coq.Numbers.NatInt.NZAddOrder]
q:10 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
q:10 [binder, in Coq.NArith.BinNat]
Q:10 [binder, in Coq.Logic.Classical_Prop]
q:10 [binder, in Coq.Reals.ClassicalConstructiveReals]
q:100 [binder, in Coq.FSets.FSetDecide]
q:100 [binder, in Coq.MSets.MSetDecide]
q:100 [binder, in Coq.Reals.ClassicalDedekindReals]
Q:1002 [binder, in Coq.Init.Specif]
q:101 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:101 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
Q:101 [binder, in Coq.Init.Specif]
q:101 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:101 [binder, in Coq.Reals.Rdefinitions]
q:1014 [binder, in Coq.Init.Specif]
Q:1018 [binder, in Coq.Init.Specif]
q:102 [binder, in Coq.Reals.Rdefinitions]
q:102 [binder, in Coq.Reals.ClassicalDedekindReals]
Q:1026 [binder, in Coq.Init.Specif]
q:103 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:103 [binder, in Coq.PArith.BinPos]
Q:1034 [binder, in Coq.Init.Specif]
q:1037 [binder, in Coq.Init.Specif]
q:104 [binder, in Coq.Numbers.Integer.Abstract.ZAddOrder]
Q:104 [binder, in Coq.Logic.Eqdep_dec]
Q:104 [binder, in Coq.ssr.ssrbool]
q:104 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:105 [binder, in Coq.ZArith.BinIntDef]
q:105 [binder, in Coq.Reals.Rtrigo1]
Q:105 [binder, in Coq.Init.Specif]
q:105 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:1051 [binder, in Coq.Init.Specif]
Q:1057 [binder, in Coq.Init.Specif]
q:106 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:106 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:106 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
q:106 [binder, in Coq.Reals.ClassicalDedekindReals]
q:107 [binder, in Coq.Reals.Rtrigo1]
q:107 [binder, in Coq.Logic.Hurkens]
q:108 [binder, in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:108 [binder, in Coq.ZArith.BinIntDef]
Q:108 [binder, in Coq.Logic.EqdepFacts]
Q:108 [binder, in Coq.ssr.ssrbool]
q:108 [binder, in Coq.Logic.Hurkens]
q:109 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
q:109 [binder, in Coq.Reals.Rtrigo1]
q:109 [binder, in Coq.Arith.Wf_nat]
q:109 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:109 [binder, in Coq.Reals.ClassicalDedekindReals]
q:11 [binder, in Coq.Arith.Le]
q:11 [binder, in Coq.QArith.Qcanon]
q:11 [binder, in Coq.Logic.EqdepFacts]
Q:11 [binder, in Coq.Logic.Berardi]
Q:11 [binder, in Coq.Logic.PropExtensionalityFacts]
q:11 [binder, in Coq.Arith.Euclid]
q:110 [binder, in Coq.ZArith.BinIntDef]
Q:110 [binder, in Coq.ssr.ssrbool]
q:110 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:110 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
q:111 [binder, in Coq.Reals.Rtrigo1]
Q:112 [binder, in Coq.Logic.EqdepFacts]
q:112 [binder, in Coq.ZArith.Zdiv]
q:112 [binder, in Coq.Reals.ClassicalDedekindReals]
Q:113 [binder, in Coq.setoid_ring.Ncring_polynom]
q:113 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:113 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
q:114 [binder, in Coq.Init.Nat]
q:115 [binder, in Coq.ZArith.BinIntDef]
q:115 [binder, in Coq.PArith.BinPos]
Q:115 [binder, in Coq.Init.Specif]
q:115 [binder, in Coq.ZArith.Zdiv]
q:115 [binder, in Coq.Vectors.Fin]
q:115 [binder, in Coq.QArith.QArith_base]
q:116 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:117 [binder, in Coq.QArith.Qcanon]
q:117 [binder, in Coq.Arith.Wf_nat]
q:118 [binder, in Coq.ZArith.Zdiv]
q:118 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:118 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
q:119 [binder, in Coq.QArith.Qcanon]
Q:119 [binder, in Coq.Init.Specif]
q:12 [binder, in Coq.QArith.Qcanon]
q:12 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
Q:12 [binder, in Coq.Logic.Classical_Prop]
q:12 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:12 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
q:12 [binder, in Coq.QArith.Qreduction]
q:12 [binder, in Coq.Reals.Cauchy.QExtra]
q:12 [binder, in Coq.Reals.ClassicalDedekindReals]
q:120 [binder, in Coq.ZArith.Zdiv]
q:121 [binder, in Coq.QArith.Qcanon]
q:121 [binder, in Coq.Reals.Rbasic_fun]
q:122 [binder, in Coq.Init.Nat]
Q:122 [binder, in Coq.ssr.ssreflect]
q:123 [binder, in Coq.ZArith.BinIntDef]
q:123 [binder, in Coq.ZArith.BinInt]
Q:123 [binder, in Coq.setoid_ring.Ncring_polynom]
q:123 [binder, in Coq.Numbers.Cyclic.Abstract.CyclicAxioms]
q:124 [binder, in Coq.PArith.BinPos]
Q:124 [binder, in Coq.ssr.ssrbool]
q:124 [binder, in Coq.PArith.BinPosDef]
q:125 [binder, in Coq.ZArith.BinIntDef]
q:125 [binder, in Coq.ZArith.BinInt]
q:125 [binder, in Coq.Arith.Wf_nat]
q:125 [binder, in Coq.ZArith.Znat]
q:127 [binder, in Coq.Logic.Eqdep_dec]
q:127 [binder, in Coq.ZArith.BinIntDef]
q:127 [binder, in Coq.ZArith.Znat]
q:129 [binder, in Coq.ZArith.BinIntDef]
q:129 [binder, in Coq.Floats.SpecFloat]
q:129 [binder, in Coq.PArith.BinPosDef]
q:13 [binder, in Coq.QArith.Qcanon]
q:13 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:13 [binder, in Coq.PArith.Pnat]
q:13 [binder, in Coq.Logic.HLevels]
q:13 [binder, in Coq.Structures.EqualitiesFacts]
q:13 [binder, in Coq.Reals.Cauchy.QExtra]
q:13 [binder, in Coq.rtauto.Rtauto]
q:131 [binder, in Coq.setoid_ring.Ring_polynom]
Q:131 [binder, in Coq.Init.Specif]
q:131 [binder, in Coq.ZArith.Znat]
Q:132 [binder, in Coq.ssr.ssrbool]
Q:133 [binder, in Coq.Logic.Eqdep_dec]
q:133 [binder, in Coq.ZArith.Znat]
q:134 [binder, in Coq.PArith.BinPos]
q:134 [binder, in Coq.ZArith.BinInt]
q:134 [binder, in Coq.micromega.OrderedRing]
q:134 [binder, in Coq.PArith.BinPosDef]
q:135 [binder, in Coq.QArith.Qcanon]
q:136 [binder, in Coq.PArith.BinPos]
q:136 [binder, in Coq.ZArith.Znumtheory]
Q:137 [binder, in Coq.Init.Specif]
q:137 [binder, in Coq.QArith.QArith_base]
q:137 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:138 [binder, in Coq.PArith.BinPos]
q:138 [binder, in Coq.ZArith.BinInt]
q:138 [binder, in Coq.micromega.OrderedRing]
q:138 [binder, in Coq.QArith.QArith_base]
Q:139 [binder, in Coq.ssr.ssrbool]
q:139 [binder, in Coq.PArith.BinPosDef]
q:14 [binder, in Coq.setoid_ring.Field_theory]
Q:14 [binder, in Coq.Numbers.Cyclic.Abstract.NZCyclic]
q:14 [binder, in Coq.Numbers.Natural.Abstract.NMulOrder]
Q:14 [binder, in Coq.Logic.Classical_Prop]
q:14 [binder, in Coq.QArith.Qreduction]
q:14 [binder, in Coq.Reals.Cauchy.QExtra]
q:14 [binder, in Coq.Reals.ClassicalDedekindReals]
q:140 [binder, in Coq.PArith.BinPos]
q:141 [binder, in Coq.ZArith.Znumtheory]
q:141 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:142 [binder, in Coq.micromega.OrderedRing]
q:143 [binder, in Coq.PArith.BinPos]
q:143 [binder, in Coq.ZArith.Znumtheory]
q:146 [binder, in Coq.PArith.BinPos]
q:146 [binder, in Coq.micromega.OrderedRing]
q:148 [binder, in Coq.QArith.QArith_base]
q:148 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:149 [binder, in Coq.PArith.BinPos]
q:149 [binder, in Coq.QArith.QArith_base]
q:15 [binder, in Coq.Logic.EqdepFacts]
q:15 [binder, in Coq.ZArith.Zpow_facts]
q:15 [binder, in Coq.PArith.Pnat]
q:15 [binder, in Coq.Logic.ProofIrrelevanceFacts]
q:15 [binder, in Coq.Reals.Cauchy.QExtra]
q:15 [binder, in Coq.Reals.ClassicalDedekindReals]
q:150 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]
q:151 [binder, in Coq.PArith.BinPos]
q:152 [binder, in Coq.Logic.Eqdep_dec]
q:153 [binder, in Coq.PArith.BinPos]
q:156 [binder, in Coq.PArith.BinPos]
q:156 [binder, in Coq.ZArith.BinInt]
q:156 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:158 [binder, in Coq.PArith.BinPos]
q:158 [binder, in Coq.NArith.BinNat]
q:16 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
q:16 [binder, in Coq.QArith.Qfield]
q:16 [binder, in Coq.QArith.Qabs]
Q:16 [binder, in Coq.Logic.Classical_Prop]
q:16 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
Q:16 [binder, in Coq.Logic.Diaconescu]
q:16 [binder, in Coq.Arith.Euclid]
q:16 [binder, in Coq.Reals.Cauchy.QExtra]
q:16 [binder, in Coq.Reals.ClassicalDedekindReals]
Q:160 [binder, in Coq.ssr.ssrfun]
q:161 [binder, in Coq.PArith.BinPos]
q:162 [binder, in Coq.NArith.BinNat]
q:163 [binder, in Coq.FSets.FMapPositive]
q:164 [binder, in Coq.PArith.BinPos]
q:164 [binder, in Coq.Structures.GenericMinMax]
q:166 [binder, in Coq.Vectors.Fin]
q:166 [binder, in Coq.ZArith.Znumtheory]
q:167 [binder, in Coq.PArith.BinPos]
q:167 [binder, in Coq.ZArith.Zorder]
q:168 [binder, in Coq.FSets.FMapPositive]
q:168 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
Q:17 [binder, in Coq.FSets.FSetDecide]
q:17 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:17 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:17 [binder, in Coq.PArith.Pnat]
Q:17 [binder, in Coq.MSets.MSetDecide]
q:17 [binder, in Coq.Arith.Cantor]
q:17 [binder, in Coq.ZArith.Zdiv]
q:17 [binder, in Coq.Reals.Cauchy.QExtra]
q:170 [binder, in Coq.PArith.BinPos]
q:171 [binder, in Coq.ZArith.Zorder]
Q:172 [binder, in Coq.micromega.ZifyClasses]
q:172 [binder, in Coq.PArith.BinPos]
q:173 [binder, in Coq.ZArith.BinInt]
q:173 [binder, in Coq.Vectors.Fin]
q:173 [binder, in Coq.ZArith.Znumtheory]
Q:174 [binder, in Coq.micromega.ZifyClasses]
Q:174 [binder, in Coq.ssr.ssrfun]
Q:176 [binder, in Coq.Logic.ChoiceFacts]
q:176 [binder, in Coq.Vectors.Fin]
Q:179 [binder, in Coq.micromega.ZifyClasses]
q:18 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:18 [binder, in Coq.Numbers.Natural.Abstract.NMulOrder]
Q:18 [binder, in Coq.Logic.Classical_Prop]
Q:18 [binder, in Coq.Logic.Diaconescu]
q:18 [binder, in Coq.QArith.Qreduction]
q:18 [binder, in Coq.Reals.Cauchy.QExtra]
q:180 [binder, in Coq.setoid_ring.Ring_theory]
q:180 [binder, in Coq.QArith.QArith_base]
Q:181 [binder, in Coq.ssr.ssrbool]
q:183 [binder, in Coq.QArith.QArith_base]
Q:187 [binder, in Coq.Logic.ChoiceFacts]
q:189 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:189 [binder, in Coq.micromega.ZMicromega]
Q:19 [binder, in Coq.FSets.FSetDecide]
q:19 [binder, in Coq.Numbers.HexadecimalPos]
q:19 [binder, in Coq.ZArith.BinInt]
q:19 [binder, in Coq.PArith.Pnat]
Q:19 [binder, in Coq.MSets.MSetDecide]
Q:19 [binder, in Coq.Init.Specif]
q:19 [binder, in Coq.ZArith.Zpow_alt]
q:19 [binder, in Coq.Numbers.DecimalPos]
q:19 [binder, in Coq.Arith.Mult]
q:19 [binder, in Coq.Reals.Cauchy.QExtra]
q:190 [binder, in Coq.ZArith.BinInt]
q:190 [binder, in Coq.Init.Specif]
q:191 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
Q:192 [binder, in Coq.Logic.ChoiceFacts]
q:193 [binder, in Coq.ZArith.BinInt]
q:193 [binder, in Coq.ZArith.Zorder]
q:193 [binder, in Coq.Structures.OrderedType]
q:193 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:194 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:194 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
q:195 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
q:196 [binder, in Coq.PArith.BinPos]
q:196 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:197 [binder, in Coq.ZArith.Zorder]
q:198 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
Q:2 [binder, in Coq.FSets.FSetDecide]
q:2 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
Q:2 [binder, in Coq.Logic.PropExtensionality]
Q:2 [binder, in Coq.MSets.MSetDecide]
Q:2 [binder, in Coq.ssr.ssrfun]
q:2 [binder, in Coq.rtauto.Bintree]
q:2 [binder, in Coq.Numbers.Integer.NatPairs.ZNatPairs]
Q:2 [binder, in Coq.Logic.Diaconescu]
q:2 [binder, in Coq.Numbers.NatInt.NZMulOrder]
q:2 [binder, in Coq.Reals.Cauchy.PosExtra]
q:20 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
q:20 [binder, in Coq.Numbers.NatInt.NZAddOrder]
q:20 [binder, in Coq.btauto.Algebra]
q:20 [binder, in Coq.setoid_ring.Field_theory]
Q:20 [binder, in Coq.Logic.Classical_Prop]
q:20 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
Q:20 [binder, in Coq.Logic.Diaconescu]
q:20 [binder, in Coq.QArith.Qreduction]
q:20 [binder, in Coq.Reals.Cauchy.QExtra]
q:20 [binder, in Coq.Reals.ClassicalDedekindReals]
q:20 [binder, in Coq.Reals.ClassicalConstructiveReals]
q:20 [binder, in Coq.QArith.QArith_base]
Q:200 [binder, in Coq.setoid_ring.Ring_polynom]
q:200 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:203 [binder, in Coq.Init.Specif]
Q:21 [binder, in Coq.FSets.FSetDecide]
q:21 [binder, in Coq.ZArith.BinInt]
q:21 [binder, in Coq.PArith.Pnat]
Q:21 [binder, in Coq.MSets.MSetDecide]
q:21 [binder, in Coq.Logic.ProofIrrelevanceFacts]
Q:21 [binder, in Coq.Logic.HLevels]
q:21 [binder, in Coq.Reals.Cauchy.QExtra]
q:214 [binder, in Coq.Init.Specif]
q:215 [binder, in Coq.PArith.BinPos]
Q:217 [binder, in Coq.Logic.EqdepFacts]
q:218 [binder, in Coq.PArith.BinPos]
q:22 [binder, in Coq.Logic.EqdepFacts]
q:22 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:22 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
Q:22 [binder, in Coq.Logic.Classical_Prop]
Q:22 [binder, in Coq.Logic.Diaconescu]
q:22 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
q:22 [binder, in Coq.QArith.Qreduction]
q:22 [binder, in Coq.Reals.Cauchy.QExtra]
q:22 [binder, in Coq.Reals.ClassicalConstructiveReals]
q:22 [binder, in Coq.QArith.QArith_base]
q:22 [binder, in Coq.rtauto.Rtauto]
q:220 [binder, in Coq.PArith.BinPos]
Q:221 [binder, in Coq.Logic.ClassicalFacts]
q:222 [binder, in Coq.PArith.BinPos]
Q:223 [binder, in Coq.Logic.EqdepFacts]
q:223 [binder, in Coq.micromega.ZMicromega]
q:225 [binder, in Coq.Init.Specif]
q:225 [binder, in Coq.setoid_ring.Field_theory]
Q:226 [binder, in Coq.setoid_ring.Ring_polynom]
Q:227 [binder, in Coq.Logic.EqdepFacts]
q:228 [binder, in Coq.PArith.BinPos]
Q:229 [binder, in Coq.micromega.EnvRing]
q:23 [binder, in Coq.PArith.BinPos]
q:23 [binder, in Coq.PArith.Pnat]
q:23 [binder, in Coq.Structures.DecidableType]
Q:23 [binder, in Coq.Logic.HLevels]
q:23 [binder, in Coq.Numbers.NatInt.NZMul]
q:23 [binder, in Coq.QArith.Qreduction]
q:23 [binder, in Coq.Reals.Cauchy.QExtra]
q:23 [binder, in Coq.ZArith.Zcompare]
q:230 [binder, in Coq.PArith.BinPos]
Q:231 [binder, in Coq.Logic.EqdepFacts]
Q:233 [binder, in Coq.Vectors.VectorSpec]
q:233 [binder, in Coq.PArith.BinPos]
q:235 [binder, in Coq.Init.Specif]
q:236 [binder, in Coq.PArith.BinPos]
q:238 [binder, in Coq.PArith.BinPos]
q:24 [binder, in Coq.QArith.Qcanon]
q:24 [binder, in Coq.Numbers.NatInt.NZAddOrder]
q:24 [binder, in Coq.ZArith.BinInt]
q:24 [binder, in Coq.Reals.Abstract.ConstructiveLimits]
Q:24 [binder, in Coq.Logic.Classical_Prop]
q:24 [binder, in Coq.Numbers.NatInt.NZDiv]
q:24 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:24 [binder, in Coq.Reals.ClassicalDedekindReals]
q:24 [binder, in Coq.QArith.QArith_base]
q:241 [binder, in Coq.PArith.BinPos]
q:242 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
q:243 [binder, in Coq.PArith.BinPos]
q:243 [binder, in Coq.Init.Specif]
q:246 [binder, in Coq.Numbers.Cyclic.Int31.Cyclic31]
q:246 [binder, in Coq.PArith.BinPos]
q:248 [binder, in Coq.PArith.BinPos]
q:25 [binder, in Coq.PArith.Pnat]
q:25 [binder, in Coq.Reals.Abstract.ConstructiveAbs]
q:25 [binder, in Coq.Numbers.NatInt.NZAdd]
q:25 [binder, in Coq.Reals.Cauchy.QExtra]
q:250 [binder, in Coq.PArith.BinPos]
q:250 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]
q:251 [binder, in Coq.Init.Specif]
q:251 [binder, in Coq.QArith.QArith_base]
q:255 [binder, in Coq.Logic.EqdepFacts]
q:255 [binder, in Coq.PArith.BinPos]
q:255 [binder, in Coq.QArith.QArith_base]
q:256 [binder, in Coq.Init.Specif]
q:257 [binder, in Coq.QArith.QArith_base]
q:258 [binder, in Coq.PArith.BinPos]
q:259 [binder, in Coq.QArith.QArith_base]
q:26 [binder, in Coq.QArith.Qcanon]
q:26 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:26 [binder, in Coq.ZArith.BinInt]
Q:26 [binder, in Coq.Logic.Classical_Prop]
q:26 [binder, in Coq.QArith.Qpower]
q:26 [binder, in Coq.QArith.Qreduction]
q:26 [binder, in Coq.QArith.QArith_base]
q:260 [binder, in Coq.ZArith.Zdiv]
q:261 [binder, in Coq.PArith.BinPos]
q:261 [binder, in Coq.QArith.QArith_base]
q:263 [binder, in Coq.Logic.EqdepFacts]
q:263 [binder, in Coq.PArith.BinPos]
q:265 [binder, in Coq.PArith.BinPos]
q:267 [binder, in Coq.PArith.BinPos]
q:269 [binder, in Coq.PArith.BinPos]
q:27 [binder, in Coq.PArith.Pnat]
q:27 [binder, in Coq.Numbers.NatInt.NZMul]
q:27 [binder, in Coq.QArith.Qpower]
q:27 [binder, in Coq.Reals.Cauchy.QExtra]
q:270 [binder, in Coq.Logic.EqdepFacts]
q:271 [binder, in Coq.PArith.BinPos]
q:273 [binder, in Coq.PArith.BinPos]
Q:273 [binder, in Coq.Init.Specif]
q:275 [binder, in Coq.PArith.BinPos]
q:275 [binder, in Coq.Init.Specif]
Q:276 [binder, in Coq.setoid_ring.Ring_polynom]
q:277 [binder, in Coq.PArith.BinPos]
q:279 [binder, in Coq.PArith.BinPos]
q:28 [binder, in Coq.QArith.Qcanon]
q:28 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:28 [binder, in Coq.PArith.BinPos]
q:28 [binder, in Coq.Numbers.NatInt.NZAddOrder]
q:28 [binder, in Coq.ZArith.BinInt]
q:28 [binder, in Coq.ZArith.Zpow_facts]
q:28 [binder, in Coq.btauto.Algebra]
q:28 [binder, in Coq.Numbers.Cyclic.Int63.Cyclic63]
q:28 [binder, in Coq.Numbers.NatInt.NZDiv]
q:28 [binder, in Coq.Arith.Between]
q:28 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:28 [binder, in Coq.QArith.Qreduction]
q:28 [binder, in Coq.Reals.ClassicalDedekindReals]
q:28 [binder, in Coq.Reals.ClassicalConstructiveReals]
q:28 [binder, in Coq.QArith.QArith_base]
q:281 [binder, in Coq.PArith.BinPos]
q:282 [binder, in Coq.NArith.BinNat]
q:283 [binder, in Coq.PArith.BinPos]
Q:283 [binder, in Coq.setoid_ring.Ring_polynom]
Q:283 [binder, in Coq.Init.Specif]
q:285 [binder, in Coq.QArith.QArith_base]
q:287 [binder, in Coq.PArith.BinPos]
q:288 [binder, in Coq.QArith.QArith_base]
q:289 [binder, in Coq.PArith.BinPos]
Q:289 [binder, in Coq.Init.Specif]
q:29 [binder, in Coq.Logic.EqdepFacts]
q:29 [binder, in Coq.PArith.Pnat]
q:29 [binder, in Coq.Numbers.NatInt.NZAdd]
q:29 [binder, in Coq.Reals.Cauchy.QExtra]
q:290 [binder, in Coq.QArith.QArith_base]
q:292 [binder, in Coq.PArith.BinPos]
q:292 [binder, in Coq.QArith.QArith_base]
q:294 [binder, in Coq.QArith.QArith_base]
Q:295 [binder, in Coq.Init.Specif]
q:297 [binder, in Coq.PArith.BinPos]
q:297 [binder, in Coq.Init.Specif]
Q:299 [binder, in Coq.micromega.EnvRing]
q:3 [binder, in Coq.Strings.OctalString]
q:3 [binder, in Coq.Strings.HexString]
q:3 [binder, in Coq.PArith.Pnat]
Q:3 [binder, in Coq.Logic.ClassicalChoice]
q:3 [binder, in Coq.ZArith.Zdiv]
q:3 [binder, in Coq.Strings.BinaryString]
q:3 [binder, in Coq.Logic.HLevels]
Q:3 [binder, in Coq.Logic.Eqdep]
q:3 [binder, in Coq.ZArith.Znumtheory]
q:3 [binder, in Coq.Reals.Cauchy.PosExtra]
q:30 [binder, in Coq.QArith.Qcanon]
q:30 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:30 [binder, in Coq.PArith.BinPos]
q:30 [binder, in Coq.btauto.Algebra]
q:30 [binder, in Coq.Arith.Plus]
q:30 [binder, in Coq.Numbers.HexadecimalR]
q:30 [binder, in Coq.Numbers.DecimalR]
q:30 [binder, in Coq.Reals.ClassicalConstructiveReals]
q:30 [binder, in Coq.QArith.QArith_base]
q:300 [binder, in Coq.PArith.BinPos]
q:302 [binder, in Coq.PArith.BinPos]
Q:303 [binder, in Coq.Init.Logic]
q:304 [binder, in Coq.PArith.BinPos]
q:304 [binder, in Coq.ZArith.BinInt]
Q:305 [binder, in Coq.Init.Specif]
q:306 [binder, in Coq.PArith.BinPos]
q:306 [binder, in Coq.ZArith.BinInt]
q:307 [binder, in Coq.Init.Specif]
q:308 [binder, in Coq.PArith.BinPos]
q:31 [binder, in Coq.Arith.Between]
q:31 [binder, in Coq.Structures.EqualitiesFacts]
q:31 [binder, in Coq.Reals.Cauchy.QExtra]
q:31 [binder, in Coq.Reals.ClassicalDedekindReals]
q:310 [binder, in Coq.PArith.BinPos]
q:312 [binder, in Coq.PArith.BinPos]
q:313 [binder, in Coq.ZArith.BinInt]
Q:313 [binder, in Coq.Init.Logic]
q:314 [binder, in Coq.PArith.BinPos]
q:315 [binder, in Coq.ZArith.BinInt]
q:316 [binder, in Coq.PArith.BinPos]
Q:316 [binder, in Coq.Init.Specif]
q:317 [binder, in Coq.ZArith.BinInt]
q:318 [binder, in Coq.PArith.BinPos]
q:318 [binder, in Coq.Init.Specif]
q:32 [binder, in Coq.QArith.Qcanon]
q:32 [binder, in Coq.Structures.OrdersLists]
q:32 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:32 [binder, in Coq.Logic.EqdepFacts]
q:32 [binder, in Coq.PArith.BinPos]
q:32 [binder, in Coq.btauto.Algebra]
Q:32 [binder, in Coq.Init.Datatypes]
q:32 [binder, in Coq.Numbers.NatInt.NZDiv]
q:32 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
q:320 [binder, in Coq.Reals.Abstract.ConstructiveReals]
q:320 [binder, in Coq.PArith.BinPos]
q:320 [binder, in Coq.ZArith.BinInt]
q:322 [binder, in Coq.PArith.BinPos]
q:322 [binder, in Coq.ZArith.BinInt]
q:323 [binder, in Coq.Reals.Abstract.ConstructiveReals]
q:324 [binder, in Coq.PArith.BinPos]
q:324 [binder, in Coq.ZArith.BinInt]
Q:326 [binder, in Coq.Init.Specif]
q:327 [binder, in Coq.Reals.Abstract.ConstructiveReals]
q:327 [binder, in Coq.PArith.BinPos]
q:327 [binder, in Coq.ZArith.BinInt]
q:329 [binder, in Coq.Reals.Abstract.ConstructiveReals]
q:329 [binder, in Coq.ZArith.BinInt]
q:33 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:33 [binder, in Coq.PArith.Pnat]
q:33 [binder, in Coq.Numbers.HexadecimalR]
Q:33 [binder, in Coq.Logic.Classical_Prop]
q:33 [binder, in Coq.Numbers.DecimalR]
q:33 [binder, in Coq.Arith.Mult]
q:331 [binder, in Coq.Reals.Abstract.ConstructiveReals]
q:331 [binder, in Coq.ZArith.BinInt]
q:332 [binder, in Coq.PArith.BinPos]
q:332 [binder, in Coq.Init.Specif]
q:333 [binder, in Coq.ZArith.BinInt]
q:334 [binder, in Coq.PArith.BinPos]
q:335 [binder, in Coq.ZArith.BinInt]
q:336 [binder, in Coq.PArith.BinPos]
q:337 [binder, in Coq.ZArith.BinInt]
Q:338 [binder, in Coq.Init.Specif]
q:34 [binder, in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:34 [binder, in Coq.QArith.Qcanon]
q:34 [binder, in Coq.Structures.OrdersLists]
q:34 [binder, in Coq.PArith.BinPos]
q:34 [binder, in Coq.btauto.Algebra]
Q:34 [binder, in Coq.ssr.ssrbool]
q:34 [binder, in Coq.Arith.Plus]
q:34 [binder, in Coq.Arith.Between]
q:34 [binder, in Coq.QArith.Qpower]
q:34 [binder, in Coq.Reals.Cauchy.QExtra]
q:340 [binder, in Coq.ZArith.BinInt]
q:342 [binder, in Coq.ZArith.BinInt]
Q:344 [binder, in Coq.Init.Specif]
q:346 [binder, in Coq.ZArith.BinInt]
q:348 [binder, in Coq.ZArith.BinInt]
q:349 [binder, in Coq.Logic.ChoiceFacts]
q:349 [binder, in Coq.Init.Specif]
q:35 [binder, in Coq.PArith.Pnat]
q:350 [binder, in Coq.ZArith.BinInt]
q:351 [binder, in Coq.PArith.BinPos]
q:351 [binder, in Coq.Logic.ChoiceFacts]
q:352 [binder, in Coq.ZArith.BinInt]
Q:357 [binder, in Coq.Logic.ChoiceFacts]
q:358 [binder, in Coq.ZArith.BinInt]
Q:359 [binder, in Coq.Logic.ChoiceFacts]
q:36 [binder, in Coq.PArith.BinPos]
Q:36 [binder, in Coq.ssr.ssrbool]
q:36 [binder, in Coq.QArith.Qpower]
q:36 [binder, in Coq.Reals.ClassicalConstructiveReals]
q:360 [binder, in Coq.ZArith.BinInt]
Q:361 [binder, in Coq.Logic.ChoiceFacts]
q:361 [binder, in Coq.Init.Specif]
q:362 [binder, in Coq.ZArith.BinInt]
q:364 [binder, in Coq.ZArith.BinInt]
Q:364 [binder, in Coq.Logic.ChoiceFacts]
q:365 [binder, in Coq.PArith.BinPos]
q:366 [binder, in Coq.ZArith.BinInt]
Q:366 [binder, in Coq.Init.Specif]
q:367 [binder, in Coq.PArith.BinPos]
q:368 [binder, in Coq.ZArith.BinInt]
q:37 [binder, in Coq.Reals.Abstract.ConstructiveReals]
q:37 [binder, in Coq.Arith.Between]
q:370 [binder, in Coq.PArith.BinPos]
q:373 [binder, in Coq.PArith.BinPos]
q:375 [binder, in Coq.PArith.BinPos]
q:376 [binder, in Coq.ZArith.BinInt]
q:378 [binder, in Coq.PArith.BinPos]
q:378 [binder, in Coq.ZArith.BinInt]
q:38 [binder, in Coq.Logic.EqdepFacts]
q:38 [binder, in Coq.PArith.BinPos]
q:38 [binder, in Coq.Arith.Plus]
q:38 [binder, in Coq.ZArith.Zdiv]
q:38 [binder, in Coq.QArith.Qpower]
q:38 [binder, in Coq.Reals.ClassicalDedekindReals]
q:380 [binder, in Coq.ZArith.BinInt]
q:381 [binder, in Coq.PArith.BinPos]
q:382 [binder, in Coq.ZArith.BinInt]
q:384 [binder, in Coq.QArith.QArith_base]
q:385 [binder, in Coq.PArith.BinPos]
q:388 [binder, in Coq.PArith.BinPos]
q:39 [binder, in Coq.ZArith.BinInt]
q:39 [binder, in Coq.micromega.RMicromega]
q:391 [binder, in Coq.PArith.BinPos]
q:395 [binder, in Coq.PArith.BinPos]
q:398 [binder, in Coq.PArith.BinPos]
q:4 [binder, in Coq.QArith.Qcanon]
q:4 [binder, in Coq.Numbers.Integer.Abstract.ZMulOrder]
q:4 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
q:40 [binder, in Coq.Reals.Abstract.ConstructiveReals]
q:40 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
q:40 [binder, in Coq.ZArith.Zbool]
q:40 [binder, in Coq.Arith.Between]
q:40 [binder, in Coq.QArith.Qpower]
q:401 [binder, in Coq.PArith.BinPos]
q:404 [binder, in Coq.PArith.BinPos]
q:406 [binder, in Coq.Numbers.Cyclic.Int63.Uint63]
q:407 [binder, in Coq.PArith.BinPos]
q:407 [binder, in Coq.Init.Specif]
Q:409 [binder, in Coq.Init.Logic]
Q:41 [binder, in Coq.Logic.ConstructiveEpsilon]
q:41 [binder, in Coq.PArith.Pnat]
q:41 [binder, in Coq.micromega.RMicromega]
q:411 [binder, in Coq.PArith.BinPos]
q:414 [binder, in Coq.PArith.BinPos]
q:414 [binder, in Coq.Init.Specif]
Q:414 [binder, in Coq.Init.Logic]
q:417 [binder, in Coq.PArith.BinPos]
q:42 [binder, in Coq.PArith.BinPos]
q:42 [binder, in Coq.btauto.Algebra]
q:42 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:42 [binder, in Coq.Arith.Plus]
q:42 [binder, in Coq.Reals.ClassicalDedekindReals]
q:421 [binder, in Coq.PArith.BinPos]
q:422 [binder, in Coq.Init.Specif]
q:423 [binder, in Coq.PArith.BinPos]
q:427 [binder, in Coq.setoid_ring.Field_theory]
q:429 [binder, in Coq.PArith.BinPos]
q:43 [binder, in Coq.Structures.OrdersLists]
Q:43 [binder, in Coq.setoid_ring.Ring_polynom]
q:43 [binder, in Coq.Program.Equality]
q:43 [binder, in Coq.Arith.Between]
q:43 [binder, in Coq.micromega.RMicromega]
q:43 [binder, in Coq.Structures.EqualitiesFacts]
q:430 [binder, in Coq.Init.Specif]
q:431 [binder, in Coq.PArith.BinPos]
q:434 [binder, in Coq.PArith.BinPos]
Q:436 [binder, in Coq.Init.Specif]
q:436 [binder, in Coq.setoid_ring.Field_theory]
q:437 [binder, in Coq.PArith.BinPos]
q:438 [binder, in Coq.Init.Specif]
q:439 [binder, in Coq.PArith.BinPos]
q:44 [binder, in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:44 [binder, in Coq.Logic.EqdepFacts]
q:44 [binder, in Coq.Numbers.NatInt.NZAddOrder]
q:44 [binder, in Coq.Numbers.Natural.Abstract.NLcm]
q:44 [binder, in Coq.Numbers.DecimalQ]
q:44 [binder, in Coq.Numbers.HexadecimalQ]
q:441 [binder, in Coq.PArith.BinPos]
q:441 [binder, in Coq.ZArith.BinInt]
Q:441 [binder, in Coq.Init.Logic]
q:444 [binder, in Coq.PArith.BinPos]
Q:446 [binder, in Coq.Init.Specif]
q:447 [binder, in Coq.PArith.BinPos]
q:45 [binder, in Coq.PArith.BinPos]
Q:45 [binder, in Coq.micromega.EnvRing]
q:45 [binder, in Coq.micromega.RMicromega]
q:450 [binder, in Coq.PArith.BinPos]
Q:452 [binder, in Coq.Init.Specif]
q:453 [binder, in Coq.PArith.BinPos]
q:453 [binder, in Coq.ssr.ssrbool]
q:456 [binder, in Coq.PArith.BinPos]
Q:458 [binder, in Coq.Init.Specif]
q:459 [binder, in Coq.ssr.ssrbool]
q:46 [binder, in Coq.Reals.Abstract.ConstructiveReals]
Q:46 [binder, in Coq.Logic.ConstructiveEpsilon]
q:46 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:46 [binder, in Coq.Structures.EqualitiesFacts]
q:460 [binder, in Coq.Init.Specif]
q:461 [binder, in Coq.PArith.BinPos]
q:464 [binder, in Coq.PArith.BinPos]
q:467 [binder, in Coq.PArith.BinPos]
Q:468 [binder, in Coq.Init.Specif]
q:47 [binder, in Coq.Numbers.DecimalQ]
q:47 [binder, in Coq.ZArith.Zquot]
Q:47 [binder, in Coq.setoid_ring.Ncring_polynom]
q:47 [binder, in Coq.Logic.HLevels]
q:47 [binder, in Coq.Numbers.HexadecimalQ]
q:470 [binder, in Coq.Init.Specif]
q:478 [binder, in Coq.PArith.BinPos]
Q:479 [binder, in Coq.Init.Specif]
q:48 [binder, in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:48 [binder, in Coq.PArith.BinPos]
q:48 [binder, in Coq.Numbers.NatInt.NZAddOrder]
q:48 [binder, in Coq.micromega.RMicromega]
q:480 [binder, in Coq.PArith.BinPos]
q:481 [binder, in Coq.Init.Specif]
q:482 [binder, in Coq.PArith.BinPos]
q:484 [binder, in Coq.PArith.BinPos]
q:487 [binder, in Coq.PArith.BinPos]
Q:489 [binder, in Coq.Init.Specif]
q:49 [binder, in Coq.Reals.Abstract.ConstructiveReals]
q:492 [binder, in Coq.Init.Logic]
q:495 [binder, in Coq.Init.Specif]
q:495 [binder, in Coq.ssr.ssrbool]
q:499 [binder, in Coq.Init.Logic]
q:5 [binder, in Coq.QArith.Qcanon]
Q:5 [binder, in Coq.FSets.FSetDecide]
q:5 [binder, in Coq.Logic.EqdepFacts]
q:5 [binder, in Coq.PArith.Pnat]
Q:5 [binder, in Coq.MSets.MSetDecide]
q:5 [binder, in Coq.Numbers.HexadecimalR]
q:5 [binder, in Coq.Numbers.DecimalR]
q:5 [binder, in Coq.NArith.Ndiv_def]
q:5 [binder, in Coq.Arith.Euclid]
q:5 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:50 [binder, in Coq.Structures.OrdersLists]
q:50 [binder, in Coq.Logic.EqdepFacts]
q:50 [binder, in Coq.ZArith.Zpow_facts]
Q:501 [binder, in Coq.Init.Specif]
Q:507 [binder, in Coq.Init.Specif]
q:507 [binder, in Coq.Init.Logic]
q:509 [binder, in Coq.ZArith.BinInt]
q:51 [binder, in Coq.PArith.BinPos]
q:51 [binder, in Coq.setoid_ring.Field_theory]
q:51 [binder, in Coq.ZArith.Zquot]
q:511 [binder, in Coq.ZArith.BinInt]
q:512 [binder, in Coq.Init.Specif]
q:513 [binder, in Coq.ZArith.BinInt]
q:515 [binder, in Coq.Init.Logic]
q:52 [binder, in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:52 [binder, in Coq.Numbers.NatInt.NZAddOrder]
q:52 [binder, in Coq.ZArith.Zdiv]
Q:527 [binder, in Coq.Init.Logic]
q:528 [binder, in Coq.Init.Specif]
q:529 [binder, in Coq.Init.Logic]
q:53 [binder, in Coq.Structures.OrdersLists]
q:53 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:53 [binder, in Coq.ZArith.Zpow_facts]
q:534 [binder, in Coq.Reals.RIneq]
Q:538 [binder, in Coq.Init.Specif]
Q:538 [binder, in Coq.Init.Logic]
q:54 [binder, in Coq.QArith.Qcanon]
q:54 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:54 [binder, in Coq.PArith.BinPos]
Q:544 [binder, in Coq.Init.Logic]
Q:547 [binder, in Coq.Init.Specif]
q:55 [binder, in Coq.QArith.Qcanon]
Q:55 [binder, in Coq.Init.Specif]
q:55 [binder, in Coq.ZArith.Zquot]
Q:550 [binder, in Coq.Init.Logic]
q:552 [binder, in Coq.Init.Logic]
Q:556 [binder, in Coq.Init.Specif]
q:558 [binder, in Coq.PArith.BinPos]
q:56 [binder, in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:56 [binder, in Coq.Logic.EqdepFacts]
q:56 [binder, in Coq.Numbers.NatInt.NZAddOrder]
q:56 [binder, in Coq.ZArith.Zdiv]
q:56 [binder, in Coq.Reals.ClassicalDedekindReals]
q:560 [binder, in Coq.PArith.BinPos]
Q:560 [binder, in Coq.Init.Logic]
q:562 [binder, in Coq.Init.Logic]
Q:564 [binder, in Coq.Init.Specif]
q:565 [binder, in Coq.PArith.BinPos]
q:568 [binder, in Coq.PArith.BinPos]
q:57 [binder, in Coq.PArith.BinPos]
q:57 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:57 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:57 [binder, in Coq.ZArith.Zpow_facts]
q:57 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:571 [binder, in Coq.PArith.BinPos]
Q:571 [binder, in Coq.Init.Logic]
Q:572 [binder, in Coq.Init.Specif]
q:573 [binder, in Coq.PArith.BinPos]
q:573 [binder, in Coq.Init.Logic]
q:576 [binder, in Coq.PArith.BinPos]
q:58 [binder, in Coq.Structures.OrderedTypeEx]
Q:580 [binder, in Coq.Init.Specif]
Q:581 [binder, in Coq.Init.Logic]
q:586 [binder, in Coq.Init.Logic]
q:59 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:59 [binder, in Coq.ZArith.Zpow_facts]
Q:592 [binder, in Coq.Init.Specif]
Q:592 [binder, in Coq.Init.Logic]
Q:598 [binder, in Coq.Init.Logic]
q:6 [binder, in Coq.QArith.Qcanon]
q:6 [binder, in Coq.Structures.OrdersEx]
q:6 [binder, in Coq.Reals.Cauchy.ConstructiveExtra]
Q:6 [binder, in Coq.Logic.Classical_Prop]
q:6 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
q:6 [binder, in Coq.QArith.Qreduction]
q:6 [binder, in Coq.QArith.QArith_base]
q:60 [binder, in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:60 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
q:60 [binder, in Coq.PArith.BinPos]
q:60 [binder, in Coq.Numbers.NatInt.NZAddOrder]
q:60 [binder, in Coq.ZArith.Zdiv]
q:60 [binder, in Coq.Numbers.Natural.Abstract.NGcd]
q:60 [binder, in Coq.Reals.ClassicalDedekindReals]
q:60 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
Q:602 [binder, in Coq.Init.Specif]
q:603 [binder, in Coq.Init.Logic]
q:607 [binder, in Coq.PArith.BinPos]
q:61 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:61 [binder, in Coq.NArith.BinNatDef]
q:610 [binder, in Coq.Init.Specif]
q:612 [binder, in Coq.PArith.BinPos]
q:613 [binder, in Coq.Init.Logic]
q:614 [binder, in Coq.PArith.BinPos]
Q:614 [binder, in Coq.Init.Specif]
q:617 [binder, in Coq.PArith.BinPos]
q:62 [binder, in Coq.Logic.EqdepFacts]
q:62 [binder, in Coq.Numbers.NatInt.NZGcd]
q:62 [binder, in Coq.Numbers.NatInt.NZMulOrder]
q:620 [binder, in Coq.PArith.BinPos]
q:620 [binder, in Coq.Init.Specif]
Q:624 [binder, in Coq.Init.Specif]
q:63 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
q:63 [binder, in Coq.PArith.BinPos]
q:63 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
Q:63 [binder, in Coq.setoid_ring.Ncring_polynom]
q:630 [binder, in Coq.Init.Logic]
q:632 [binder, in Coq.Init.Specif]
Q:636 [binder, in Coq.Init.Specif]
Q:64 [binder, in Coq.Program.Wf]
q:64 [binder, in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:64 [binder, in Coq.ZArith.Zdiv]
q:64 [binder, in Coq.NArith.BinNatDef]
q:64 [binder, in Coq.Reals.ClassicalDedekindReals]
Q:640 [binder, in Coq.Init.Logic]
q:644 [binder, in Coq.Init.Specif]
Q:648 [binder, in Coq.Init.Specif]
q:65 [binder, in Coq.PArith.BinPos]
q:65 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:65 [binder, in Coq.Logic.JMeq]
q:65 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
q:651 [binder, in Coq.Init.Specif]
q:653 [binder, in Coq.Init.Logic]
q:66 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
q:66 [binder, in Coq.Numbers.NatInt.NZMulOrder]
q:66 [binder, in Coq.Reals.ClassicalDedekindReals]
q:660 [binder, in Coq.Init.Logic]
Q:661 [binder, in Coq.Init.Specif]
Q:665 [binder, in Coq.Init.Logic]
q:67 [binder, in Coq.PArith.BinPos]
Q:670 [binder, in Coq.Init.Specif]
Q:674 [binder, in Coq.Init.Logic]
q:677 [binder, in Coq.Init.Specif]
q:68 [binder, in Coq.Numbers.Natural.Abstract.NDiv]
q:68 [binder, in Coq.Logic.EqdepFacts]
Q:68 [binder, in Coq.Logic.Diaconescu]
Q:682 [binder, in Coq.Init.Logic]
Q:683 [binder, in Coq.Init.Specif]
q:69 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:69 [binder, in Coq.Numbers.NatInt.NZGcd]
Q:690 [binder, in Coq.Init.Logic]
Q:691 [binder, in Coq.Init.Specif]
Q:698 [binder, in Coq.Init.Logic]
Q:699 [binder, in Coq.Init.Specif]
q:7 [binder, in Coq.QArith.Qcanon]
q:7 [binder, in Coq.Numbers.DecimalQ]
q:7 [binder, in Coq.ZArith.Zdiv]
Q:7 [binder, in Coq.Logic.ProofIrrelevanceFacts]
q:7 [binder, in Coq.Numbers.HexadecimalQ]
Q:7 [binder, in Coq.Logic.PropExtensionalityFacts]
q:70 [binder, in Coq.Logic.JMeq]
q:70 [binder, in Coq.Reals.ClassicalDedekindReals]
q:706 [binder, in Coq.Init.Specif]
q:71 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
Q:710 [binder, in Coq.Init.Logic]
Q:712 [binder, in Coq.Init.Specif]
q:719 [binder, in Coq.Init.Specif]
q:72 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:72 [binder, in Coq.Reals.Rbasic_fun]
Q:720 [binder, in Coq.Init.Logic]
Q:725 [binder, in Coq.Init.Specif]
q:726 [binder, in Coq.Init.Logic]
q:73 [binder, in Coq.ZArith.Znumtheory]
q:73 [binder, in Coq.Reals.ClassicalDedekindReals]
Q:730 [binder, in Coq.Init.Logic]
q:734 [binder, in Coq.Init.Specif]
q:738 [binder, in Coq.Init.Logic]
q:74 [binder, in Coq.ZArith.Zquot]
q:74 [binder, in Coq.Numbers.NatInt.NZDiv]
Q:740 [binder, in Coq.Init.Specif]
Q:742 [binder, in Coq.Init.Logic]
q:75 [binder, in Coq.Numbers.Integer.Abstract.ZLcm]
q:750 [binder, in Coq.Init.Logic]
q:752 [binder, in Coq.Init.Specif]
Q:754 [binder, in Coq.Init.Logic]
Q:756 [binder, in Coq.Init.Specif]
q:76 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:76 [binder, in Coq.Logic.JMeq]
q:76 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
q:76 [binder, in Coq.ZArith.Znumtheory]
q:762 [binder, in Coq.Init.Logic]
Q:764 [binder, in Coq.Init.Specif]
Q:766 [binder, in Coq.Init.Logic]
q:769 [binder, in Coq.Init.Logic]
q:77 [binder, in Coq.Arith.PeanoNat]
q:77 [binder, in Coq.ZArith.Zpower]
q:77 [binder, in Coq.ZArith.Zquot]
q:77 [binder, in Coq.Numbers.NatInt.NZDiv]
Q:772 [binder, in Coq.Init.Specif]
q:775 [binder, in Coq.Init.Specif]
Q:779 [binder, in Coq.Init.Logic]
q:78 [binder, in Coq.Reals.Abstract.ConstructiveReals]
q:78 [binder, in Coq.QArith.Qcanon]
Q:78 [binder, in Coq.Logic.Eqdep_dec]
q:78 [binder, in Coq.PArith.Pnat]
Q:78 [binder, in Coq.Init.Specif]
q:78 [binder, in Coq.PArith.BinPosDef]
q:781 [binder, in Coq.Init.Logic]
q:79 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
q:79 [binder, in Coq.Numbers.Integer.Abstract.ZGcd]
q:79 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
q:791 [binder, in Coq.Init.Specif]
Q:795 [binder, in Coq.Init.Logic]
Q:797 [binder, in Coq.Init.Specif]
q:798 [binder, in Coq.Init.Logic]
q:8 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Q:8 [binder, in Coq.Init.Specif]
q:8 [binder, in Coq.Logic.HLevels]
Q:8 [binder, in Coq.Logic.Classical_Prop]
q:8 [binder, in Coq.Numbers.Integer.Abstract.ZMulOrder]
q:8 [binder, in Coq.QArith.Qreduction]
q:80 [binder, in Coq.Numbers.Cyclic.Int31.Int31]
q:80 [binder, in Coq.ZArith.Zquot]
q:80 [binder, in Coq.Numbers.NatInt.NZDiv]
q:802 [binder, in Coq.Init.Logic]
Q:809 [binder, in Coq.Init.Specif]
q:81 [binder, in Coq.PArith.Pnat]
Q:813 [binder, in Coq.Init.Logic]
Q:818 [binder, in Coq.Init.Specif]
q:82 [binder, in Coq.Numbers.NatInt.NZDiv]
q:82 [binder, in Coq.Numbers.Integer.Abstract.ZDivFloor]
Q:822 [binder, in Coq.Init.Logic]
Q:826 [binder, in Coq.Init.Specif]
q:83 [binder, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
q:83 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:83 [binder, in Coq.PArith.Pnat]
q:83 [binder, in Coq.ZArith.Zpower]
q:83 [binder, in Coq.QArith.Qpower]
Q:830 [binder, in Coq.Init.Logic]
Q:834 [binder, in Coq.Init.Specif]
q:837 [binder, in Coq.Init.Logic]
Q:84 [binder, in Coq.Init.Logic]
Q:842 [binder, in Coq.Init.Specif]
Q:844 [binder, in Coq.Init.Logic]
q:85 [binder, in Coq.PArith.Pnat]
q:85 [binder, in Coq.ZArith.Zorder]
Q:852 [binder, in Coq.Init.Logic]
Q:854 [binder, in Coq.Init.Specif]
q:86 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:86 [binder, in Coq.QArith.Qpower]
Q:860 [binder, in Coq.Init.Logic]
Q:864 [binder, in Coq.Init.Specif]
q:867 [binder, in Coq.Init.Logic]
q:87 [binder, in Coq.PArith.Pnat]
q:872 [binder, in Coq.Init.Specif]
Q:873 [binder, in Coq.Init.Logic]
Q:876 [binder, in Coq.Init.Specif]
q:880 [binder, in Coq.Init.Logic]
q:882 [binder, in Coq.Init.Specif]
Q:886 [binder, in Coq.Init.Specif]
Q:886 [binder, in Coq.Init.Logic]
q:89 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:89 [binder, in Coq.Arith.PeanoNat]
q:89 [binder, in Coq.QArith.Qpower]
q:894 [binder, in Coq.Init.Specif]
q:895 [binder, in Coq.Init.Logic]
Q:898 [binder, in Coq.Init.Specif]
q:9 [binder, in Coq.QArith.Qcanon]
q:9 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyRealsMult]
q:9 [binder, in Coq.QArith.Qreduction]
Q:90 [binder, in Coq.Init.Logic]
Q:901 [binder, in Coq.Init.Logic]
q:906 [binder, in Coq.Init.Specif]
q:91 [binder, in Coq.Numbers.Integer.Abstract.ZDivEucl]
q:91 [binder, in Coq.Reals.ClassicalDedekindReals]
q:91 [binder, in Coq.QArith.QArith_base]
Q:910 [binder, in Coq.Init.Specif]
q:913 [binder, in Coq.Init.Specif]
q:913 [binder, in Coq.Init.Logic]
Q:917 [binder, in Coq.Init.Logic]
q:92 [binder, in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:92 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
Q:92 [binder, in Coq.Init.Datatypes]
q:92 [binder, in Coq.QArith.Qpower]
Q:923 [binder, in Coq.Init.Specif]
Q:925 [binder, in Coq.Init.Logic]
q:93 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:93 [binder, in Coq.PArith.Pnat]
Q:932 [binder, in Coq.Init.Specif]
Q:933 [binder, in Coq.Init.Logic]
q:936 [binder, in Coq.Init.Logic]
q:939 [binder, in Coq.Init.Specif]
q:94 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:94 [binder, in Coq.Reals.Cauchy.ConstructiveCauchyAbs]
Q:945 [binder, in Coq.Init.Specif]
q:95 [binder, in Coq.ZArith.BinIntDef]
q:95 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:95 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:95 [binder, in Coq.Reals.ClassicalDedekindReals]
q:950 [binder, in Coq.Init.Logic]
Q:953 [binder, in Coq.Init.Specif]
Q:956 [binder, in Coq.Init.Logic]
Q:96 [binder, in Coq.Program.Wf]
q:96 [binder, in Coq.Numbers.Integer.Abstract.ZAddOrder]
q:96 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:96 [binder, in Coq.PArith.Pnat]
q:96 [binder, in Coq.Init.Nat]
q:96 [binder, in Coq.Reals.Abstract.ConstructiveRealsMorphisms]
Q:960 [binder, in Coq.Lists.List]
Q:961 [binder, in Coq.Init.Specif]
q:968 [binder, in Coq.Init.Specif]
q:97 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
q:97 [binder, in Coq.PArith.BinPosDef]
Q:974 [binder, in Coq.Init.Specif]
Q:976 [binder, in Coq.Lists.List]
q:98 [binder, in Coq.ZArith.BinIntDef]
q:98 [binder, in Coq.PArith.BinPos]
q:98 [binder, in Coq.Reals.Cauchy.ConstructiveRcomplete]
q:98 [binder, in Coq.Numbers.Integer.Abstract.ZDivTrunc]
q:98 [binder, in Coq.Arith.PeanoNat]
q:98 [binder, in Coq.Structures.GenericMinMax]
Q:98 [binder, in Coq.setoid_ring.Ncring_polynom]
q:98 [binder, in Coq.QArith.Qpower]
q:98 [binder, in Coq.Reals.Abstract.ConstructiveMinMax]
Q:980 [binder, in Coq.Lists.List]
q:981 [binder, in Coq.Init.Specif]
Q:984 [binder, in Coq.Lists.List]
Q:987 [binder, in Coq.Init.Specif]
Q:988 [binder, in Coq.Lists.List]
q:99 [binder, in Coq.Reals.Abstract.ConstructiveLUB]
Q:992 [binder, in Coq.Lists.List]
Q:996 [binder, in Coq.Lists.List]
q:996 [binder, in Coq.Init.Specif]

---

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

(72679 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

(1040 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

(47172 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

(791 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

(1553 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

(585 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

(11862 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

(1030 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

(625 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

(308 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

(474 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

(493 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

(896 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

(1443 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

(4242 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

(165 entries)