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

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

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

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

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

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

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

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

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

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

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

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

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

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

(166 entries)

---

P (abbreviation)

pairT [in Stdlib.Init.Datatypes]
Pcase [in Stdlib.PArith.BinPos]
Pcompare [in Stdlib.PArith.BinPos]
Pcompare_1 [in Stdlib.PArith.BinPos]
Pcompare_p_Sp [in Stdlib.PArith.BinPos]
Pcompare_antisym [in Stdlib.PArith.BinPos]
Pcompare_Lt_Gt [in Stdlib.PArith.BinPos]
Pcompare_eq_Lt [in Stdlib.PArith.BinPos]
Pcompare_Gt_Lt [in Stdlib.PArith.BinPos]
Pcompare_eq_iff [in Stdlib.PArith.BinPos]
Pcompare_refl_id [in Stdlib.PArith.BinPos]
Pcompare_nat_compare [in Stdlib.PArith.Pnat]
Pdouble_minus_one_o_succ_eq_xI [in Stdlib.PArith.BinPos]
Pdouble_minus_two [in Stdlib.PArith.BinPos]
Pdouble_plus_one_mask [in Stdlib.PArith.BinPos]
Pdouble_minus_one [in Stdlib.PArith.BinPos]
PeanoOne [in Stdlib.PArith.BinPos]
PeanoSucc [in Stdlib.PArith.BinPos]
peanoView [in Stdlib.PArith.BinPos]
PeanoView [in Stdlib.PArith.BinPos]
PeanoViewUnique [in Stdlib.PArith.BinPos]
PeanoView_iter [in Stdlib.PArith.BinPos]
peanoView_xI [in Stdlib.PArith.BinPos]
peanoView_xO [in Stdlib.PArith.BinPos]
PeanoView_rec [in Stdlib.PArith.BinPos]
PeanoView_ind [in Stdlib.PArith.BinPos]
PeanoView_rect [in Stdlib.PArith.BinPos]
Peqb_correct [in Stdlib.NArith.Ndec]
permutation [in Stdlib.Sorting.PermutEq]
Permutation_app_swap [in Stdlib.Sorting.Permutation]
permut_tran [in Stdlib.Sorting.PermutSetoid]
permut_right [in Stdlib.Sorting.PermutSetoid]
PExpr [in Stdlib.micromega.EnvRing]
Pge_ge [in Stdlib.PArith.Pnat]
Pgt_gt [in Stdlib.PArith.Pnat]
ph [in Stdlib.ssr.ssrbool]
ph [in Stdlib.ssr.ssrbool]
phi_pos1 [in Stdlib.micromega.ZCoeff]
phi_pos [in Stdlib.micromega.ZCoeff]
Pind [in Stdlib.PArith.BinPos]
Ple_le [in Stdlib.PArith.Pnat]
Plt_not_plus_l [in Stdlib.PArith.BinPos]
Plt_plus_r [in Stdlib.PArith.BinPos]
Plt_1 [in Stdlib.PArith.BinPos]
Plt_lt [in Stdlib.PArith.Pnat]
plus [in Stdlib.Init.Peano]
plus_lt_is_lt [in Stdlib.Reals.RIneq]
plus_le_is_le [in Stdlib.Reals.RIneq]
plus_succ_r_reverse [in Stdlib.Init.Peano]
plus_0_r_reverse [in Stdlib.Init.Peano]
Pminus [in Stdlib.PArith.BinPos]
Pminus_Eq [in Stdlib.PArith.BinPos]
Pminus_Lt [in Stdlib.PArith.BinPos]
Pminus_mask_Lt [in Stdlib.PArith.BinPos]
Pminus_minus_distr [in Stdlib.PArith.BinPos]
Pminus_plus_distr [in Stdlib.PArith.BinPos]
Pminus_xI_xI [in Stdlib.PArith.BinPos]
Pminus_decr [in Stdlib.PArith.BinPos]
Pminus_lt_mono_r [in Stdlib.PArith.BinPos]
Pminus_compare_mono_r [in Stdlib.PArith.BinPos]
Pminus_compare_mono_l [in Stdlib.PArith.BinPos]
Pminus_lt_mono_l [in Stdlib.PArith.BinPos]
Pminus_mask_diag [in Stdlib.PArith.BinPos]
Pminus_succ_r [in Stdlib.PArith.BinPos]
Pminus_mask_carry_spec [in Stdlib.PArith.BinPos]
Pminus_mask_succ_r [in Stdlib.PArith.BinPos]
Pminus_mask_carry [in Stdlib.PArith.BinPos]
Pminus_mask [in Stdlib.PArith.BinPos]
Pminus_minus [in Stdlib.PArith.Pnat]
Pmult [in Stdlib.PArith.BinPos]
Pmult_minus_distr_l [in Stdlib.PArith.BinPos]
Pmult_le_mono [in Stdlib.PArith.BinPos]
Pmult_le_mono_r [in Stdlib.PArith.BinPos]
Pmult_le_mono_l [in Stdlib.PArith.BinPos]
Pmult_lt_mono [in Stdlib.PArith.BinPos]
Pmult_lt_mono_r [in Stdlib.PArith.BinPos]
Pmult_lt_mono_l [in Stdlib.PArith.BinPos]
Pmult_compare_mono_r [in Stdlib.PArith.BinPos]
Pmult_compare_mono_l [in Stdlib.PArith.BinPos]
Pmult_1_inversion_l [in Stdlib.PArith.BinPos]
Pmult_reg_l [in Stdlib.PArith.BinPos]
Pmult_reg_r [in Stdlib.PArith.BinPos]
Pmult_xO_discr [in Stdlib.PArith.BinPos]
Pmult_xI_mult_xO_discr [in Stdlib.PArith.BinPos]
Pmult_assoc [in Stdlib.PArith.BinPos]
Pmult_plus_distr_r [in Stdlib.PArith.BinPos]
Pmult_plus_distr_l [in Stdlib.PArith.BinPos]
Pmult_comm [in Stdlib.PArith.BinPos]
Pmult_xI_permute_r [in Stdlib.PArith.BinPos]
Pmult_xO_permute_r [in Stdlib.PArith.BinPos]
Pmult_Sn_m [in Stdlib.PArith.BinPos]
Pmult_1_r [in Stdlib.PArith.BinPos]
Pmult_nat [in Stdlib.PArith.BinPos]
Pmult_mult [in Stdlib.PArith.Pnat]
Pol [in Stdlib.micromega.EnvRing]
Poption [in Stdlib.rtauto.Bintree]
positive [in Stdlib.PArith.BinPos]
PositiveSet.InL [in Stdlib.MSets.MSetPositive]
PositiveSet.InL [in Stdlib.FSets.FSetPositive]
PositiveSet.lex [in Stdlib.MSets.MSetPositive]
PositiveSet.lex [in Stdlib.FSets.FSetPositive]
positive_eq_dec [in Stdlib.PArith.BinPos]
positive_mask_rec [in Stdlib.PArith.BinPos]
positive_mask_ind [in Stdlib.PArith.BinPos]
positive_mask_rect [in Stdlib.PArith.BinPos]
positive_mask [in Stdlib.PArith.BinPos]
positive_ind [in Stdlib.PArith.BinPos]
positive_rec [in Stdlib.PArith.BinPos]
positive_rect [in Stdlib.PArith.BinPos]
pos_mod_int [in Stdlib.Numbers.Cyclic.Int63.Cyclic63]
Pos.mul_eq_1 [in Stdlib.PArith.BinPos]
Pos.sixteen [in Stdlib.PArith.BinPosDef]
Pos.ten [in Stdlib.PArith.BinPosDef]
Power [in Stdlib.Wellfounded.Lexicographic_Exponentiation]
powerRZ_mult_distr [in Stdlib.Reals.Rfunctions]
powerRZ_neg [in Stdlib.Reals.Rfunctions]
powerRZ_inv [in Stdlib.Reals.Rfunctions]
Pplus [in Stdlib.PArith.BinPos]
Pplus_minus_assoc [in Stdlib.PArith.BinPos]
Pplus_minus_eq [in Stdlib.PArith.BinPos]
Pplus_le_mono [in Stdlib.PArith.BinPos]
Pplus_le_mono_r [in Stdlib.PArith.BinPos]
Pplus_le_mono_l [in Stdlib.PArith.BinPos]
Pplus_lt_mono [in Stdlib.PArith.BinPos]
Pplus_lt_mono_r [in Stdlib.PArith.BinPos]
Pplus_lt_mono_l [in Stdlib.PArith.BinPos]
Pplus_compare_mono_r [in Stdlib.PArith.BinPos]
Pplus_compare_mono_l [in Stdlib.PArith.BinPos]
Pplus_diag [in Stdlib.PArith.BinPos]
Pplus_xO_double_minus_one [in Stdlib.PArith.BinPos]
Pplus_xI_double_minus_one [in Stdlib.PArith.BinPos]
Pplus_xO [in Stdlib.PArith.BinPos]
Pplus_assoc [in Stdlib.PArith.BinPos]
Pplus_carry_reg_l [in Stdlib.PArith.BinPos]
Pplus_carry_reg_r [in Stdlib.PArith.BinPos]
Pplus_reg_l [in Stdlib.PArith.BinPos]
Pplus_reg_r [in Stdlib.PArith.BinPos]
Pplus_carry_plus [in Stdlib.PArith.BinPos]
Pplus_no_neutral [in Stdlib.PArith.BinPos]
Pplus_succ_permute_l [in Stdlib.PArith.BinPos]
Pplus_succ_permute_r [in Stdlib.PArith.BinPos]
Pplus_comm [in Stdlib.PArith.BinPos]
Pplus_carry_spec [in Stdlib.PArith.BinPos]
Pplus_carry [in Stdlib.PArith.BinPos]
Pplus_plus [in Stdlib.PArith.Pnat]
Ppred_Nsucc [in Stdlib.NArith.BinNat]
Ppred_N_spec [in Stdlib.NArith.BinNat]
Prec [in Stdlib.PArith.BinPos]
Prect [in Stdlib.PArith.BinPos]
Prect_base [in Stdlib.PArith.BinPos]
Prect_succ [in Stdlib.PArith.BinPos]
pred [in Stdlib.Init.Peano]
predicate [in Stdlib.Classes.RelationClasses]
PredicateExtensionality [in Stdlib.Logic.PropExtensionalityFacts]
pred_of_simpl [in Stdlib.ssr.ssrbool]
pred_o_P_of_succ_nat_o_nat_of_P_eq_id [in Stdlib.PArith.Pnat]
prodT [in Stdlib.Init.Datatypes]
prodT_ind [in Stdlib.Init.Datatypes]
prodT_rec [in Stdlib.Init.Datatypes]
prodT_rect [in Stdlib.Init.Datatypes]
prod_f_SO [in Stdlib.Reals.Rprod]
prod_neq_R0 [in Stdlib.Reals.RIneq]
prod_length [in Stdlib.Lists.List]
PropositionalExtensionality [in Stdlib.Logic.PropExtensionalityFacts]
PropositionalFunctionalExtensionality [in Stdlib.Logic.PropExtensionalityFacts]
ProvablePropositionExtensionality [in Stdlib.Logic.PropExtensionalityFacts]
Psize [in Stdlib.PArith.BinPos]
Psize_pos_le [in Stdlib.PArith.BinPos]
Psize_pos_gt [in Stdlib.PArith.BinPos]
Psize_monotone [in Stdlib.PArith.BinPos]
Psize_pos [in Stdlib.PArith.BinPos]
Psquare_correct [in Stdlib.ZArith.Zpow_facts]
Psucc_pred [in Stdlib.PArith.BinPos]
Psucc_not_one [in Stdlib.PArith.BinPos]
Psucc_o_double_minus_one_eq_xO [in Stdlib.PArith.BinPos]
Psucc_S [in Stdlib.PArith.Pnat]
push [in Stdlib.micromega.Tauto]
P_of_succ_nat [in Stdlib.PArith.BinPos]
P_of_succ_nat_o_nat_of_P_eq_succ [in Stdlib.PArith.Pnat]
P_of_succ_nat_of_P [in Stdlib.PArith.Pnat]
P_Rmin [in Stdlib.Reals.Rpower]

---

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(166 entries)