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

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

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

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

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

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

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

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

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

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

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

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

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

(4910 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)

---

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]
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]
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_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]
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]
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]
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]
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]
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.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]
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_of_RcstR [lemma, in Coq.micromega.RMicromega]
Q_of_Rcst [definition, in Coq.micromega.RMicromega]
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.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]
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]

---

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

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

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

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

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

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

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

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

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

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

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

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

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

(4910 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)