| 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 | (26611 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 | (1022 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 | (806 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 | (1548 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 | (595 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 | (12054 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 | (959 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 | (629 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 | (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 | (505 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 | (912 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 | (1508 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 | (5124 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) |
O
O [constructor, in Coq.Init.Datatypes]oapp [abbreviation, in Coq.ssr.ssrfun]
oappEmap [lemma, in Coq.ssr.ssrfun]
oapp_comp_f [lemma, in Coq.ssr.ssrfun]
oapp_comp [lemma, in Coq.ssr.ssrfun]
obind [abbreviation, in Coq.ssr.ssrfun]
obindEapp [lemma, in Coq.ssr.ssrfun]
ObsoletePmultNat [section, in Coq.PArith.Pnat]
ocancel [definition, in Coq.ssr.ssrfun]
ocan_in_comp [lemma, in Coq.ssr.ssrbool]
ocan_comp [lemma, in Coq.ssr.ssrfun]
ocons [definition, in Coq.micromega.Tauto]
OctalString [library]
odd [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
Odd [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
odd [definition, in Coq.Init.Nat]
odd [abbreviation, in Coq.Arith.Even]
odd_bitwise [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
odd_spec [abbreviation, in Coq.Numbers.Natural.Peano.NPeano]
odd_S2n [abbreviation, in Coq.Arith.Div2]
odd_S2n_stt [definition, in Coq.Arith.Div2]
odd_double [abbreviation, in Coq.Arith.Div2]
odd_double_stt [definition, in Coq.Arith.Div2]
odd_div2 [abbreviation, in Coq.Arith.Div2]
odd_div2_stt [definition, in Coq.Arith.Div2]
odd_mult_inv_r [abbreviation, in Coq.Arith.Even]
odd_mult_inv_r_stt [definition, in Coq.Arith.Even]
odd_mult_inv_l [abbreviation, in Coq.Arith.Even]
odd_mult_inv_l_stt [definition, in Coq.Arith.Even]
odd_mult [abbreviation, in Coq.Arith.Even]
odd_mult_stt [definition, in Coq.Arith.Even]
odd_plus_odd_inv_r [abbreviation, in Coq.Arith.Even]
odd_plus_odd_inv_r_stt [definition, in Coq.Arith.Even]
odd_plus_odd_inv_l [abbreviation, in Coq.Arith.Even]
odd_plus_odd_inv_l_stt [definition, in Coq.Arith.Even]
odd_plus_even_inv_r [abbreviation, in Coq.Arith.Even]
odd_plus_even_inv_r_stt [definition, in Coq.Arith.Even]
odd_plus_even_inv_l [abbreviation, in Coq.Arith.Even]
odd_plus_even_inv_l_stt [definition, in Coq.Arith.Even]
odd_even_plus [abbreviation, in Coq.Arith.Even]
odd_even_plus_stt [definition, in Coq.Arith.Even]
odd_plus_r [abbreviation, in Coq.Arith.Even]
odd_plus_r_stt [definition, in Coq.Arith.Even]
odd_plus_l [abbreviation, in Coq.Arith.Even]
odd_plus_l_stt [definition, in Coq.Arith.Even]
odd_plus_split [abbreviation, in Coq.Arith.Even]
odd_plus_split_stt [definition, in Coq.Arith.Even]
odd_equiv [abbreviation, in Coq.Arith.Even]
odd_sind [abbreviation, in Coq.Arith.Even]
odd_ind [abbreviation, in Coq.Arith.Even]
odd_S [abbreviation, in Coq.Arith.Even]
odd_even_lem [abbreviation, in Coq.Arith.Mult]
odd_even_lem_stt [definition, in Coq.Arith.Mult]
odflt [abbreviation, in Coq.ssr.ssrfun]
OEQ [constructor, in Coq.Structures.OrdersTac]
of_list_to_list_opp [lemma, in Coq.Vectors.VectorSpec]
of_pos [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
of_bits_to_bits [lemma, in Coq.Init.Byte]
of_bits [definition, in Coq.Init.Byte]
of_list_inj [lemma, in Coq.Numbers.DecimalFacts]
of_list_to_list [lemma, in Coq.Numbers.DecimalFacts]
of_list [definition, in Coq.Numbers.DecimalFacts]
of_nat_0 [definition, in Coq.Strings.OctalString]
of_Z_m1 [definition, in Coq.Strings.OctalString]
of_Z_0 [definition, in Coq.Strings.OctalString]
of_N_0 [definition, in Coq.Strings.OctalString]
of_pos_8 [definition, in Coq.Strings.OctalString]
of_pos_7 [definition, in Coq.Strings.OctalString]
of_pos_3 [definition, in Coq.Strings.OctalString]
of_pos_2 [definition, in Coq.Strings.OctalString]
of_pos_1 [definition, in Coq.Strings.OctalString]
of_nat [definition, in Coq.Strings.OctalString]
of_Z [definition, in Coq.Strings.OctalString]
of_N [definition, in Coq.Strings.OctalString]
of_pos [definition, in Coq.Strings.OctalString]
of_nat_0 [definition, in Coq.Strings.HexString]
of_Z_m1 [definition, in Coq.Strings.HexString]
of_Z_0 [definition, in Coq.Strings.HexString]
of_N_0 [definition, in Coq.Strings.HexString]
of_pos_16 [definition, in Coq.Strings.HexString]
of_pos_15 [definition, in Coq.Strings.HexString]
of_pos_14 [definition, in Coq.Strings.HexString]
of_pos_13 [definition, in Coq.Strings.HexString]
of_pos_12 [definition, in Coq.Strings.HexString]
of_pos_11 [definition, in Coq.Strings.HexString]
of_pos_10 [definition, in Coq.Strings.HexString]
of_pos_9 [definition, in Coq.Strings.HexString]
of_pos_8 [definition, in Coq.Strings.HexString]
of_pos_7 [definition, in Coq.Strings.HexString]
of_pos_3 [definition, in Coq.Strings.HexString]
of_pos_2 [definition, in Coq.Strings.HexString]
of_pos_1 [definition, in Coq.Strings.HexString]
of_nat [definition, in Coq.Strings.HexString]
of_Z [definition, in Coq.Strings.HexString]
of_N [definition, in Coq.Strings.HexString]
of_pos [definition, in Coq.Strings.HexString]
of_uint63 [axiom, in Coq.Floats.PrimFloat]
of_iff [lemma, in Coq.Numbers.DecimalQ]
of_inj [lemma, in Coq.Numbers.DecimalQ]
of_decimal_dnorm [lemma, in Coq.Numbers.DecimalQ]
of_to [lemma, in Coq.Numbers.DecimalQ]
of_IQmake_to_decimal' [lemma, in Coq.Numbers.DecimalQ]
of_IQmake_to_decimal [lemma, in Coq.Numbers.DecimalQ]
of_num_int [definition, in Coq.Init.Nat]
of_hex_int [definition, in Coq.Init.Nat]
of_int [definition, in Coq.Init.Nat]
of_num_uint [definition, in Coq.Init.Nat]
of_hex_uint [definition, in Coq.Init.Nat]
of_hex_uint_acc [definition, in Coq.Init.Nat]
of_uint [definition, in Coq.Init.Nat]
of_uint_acc [definition, in Coq.Init.Nat]
of_nat_inj [lemma, in Coq.Arith.Cantor]
of_nat [definition, in Coq.Arith.Cantor]
of_voidK [lemma, in Coq.ssr.ssrfun]
of_void [definition, in Coq.ssr.ssrfun]
of_number [definition, in Coq.Reals.Rdefinitions]
of_hexadecimal [definition, in Coq.Reals.Rdefinitions]
of_decimal [definition, in Coq.Reals.Rdefinitions]
of_int_iter_D0 [lemma, in Coq.Numbers.DecimalZ]
of_uint_iter_D0 [lemma, in Coq.Numbers.DecimalZ]
of_iff [lemma, in Coq.Numbers.DecimalZ]
of_inj [lemma, in Coq.Numbers.DecimalZ]
of_int_norm [lemma, in Coq.Numbers.DecimalZ]
of_to [lemma, in Coq.Numbers.DecimalZ]
of_list_inj [lemma, in Coq.Numbers.HexadecimalFacts]
of_list_to_list [lemma, in Coq.Numbers.HexadecimalFacts]
of_list [definition, in Coq.Numbers.HexadecimalFacts]
of_nat_0 [definition, in Coq.Strings.BinaryString]
of_Z_m1 [definition, in Coq.Strings.BinaryString]
of_Z_0 [definition, in Coq.Strings.BinaryString]
of_N_0 [definition, in Coq.Strings.BinaryString]
of_pos_3 [definition, in Coq.Strings.BinaryString]
of_pos_2 [definition, in Coq.Strings.BinaryString]
of_pos_1 [definition, in Coq.Strings.BinaryString]
of_nat [definition, in Coq.Strings.BinaryString]
of_Z [definition, in Coq.Strings.BinaryString]
of_N [definition, in Coq.Strings.BinaryString]
of_pos [definition, in Coq.Strings.BinaryString]
of_hex_int_double [lemma, in Coq.Numbers.HexadecimalZ]
of_hex_int_iter_D0 [lemma, in Coq.Numbers.HexadecimalZ]
of_hex_uint_iter_D0 [lemma, in Coq.Numbers.HexadecimalZ]
of_iff [lemma, in Coq.Numbers.HexadecimalZ]
of_inj [lemma, in Coq.Numbers.HexadecimalZ]
of_int_norm [lemma, in Coq.Numbers.HexadecimalZ]
of_to [lemma, in Coq.Numbers.HexadecimalZ]
of_nat_to_nat_inv [lemma, in Coq.Vectors.Fin]
of_nat_ext [lemma, in Coq.Vectors.Fin]
of_nat_lt [definition, in Coq.Vectors.Fin]
of_nat [definition, in Coq.Vectors.Fin]
of_iff [lemma, in Coq.Numbers.HexadecimalR]
of_inj [lemma, in Coq.Numbers.HexadecimalR]
of_hexadecimal_dnorm [lemma, in Coq.Numbers.HexadecimalR]
of_to [lemma, in Coq.Numbers.HexadecimalR]
of_IQmake_to_hexadecimal [lemma, in Coq.Numbers.HexadecimalR]
of_nat_via_N [lemma, in Coq.Strings.Byte]
of_N_via_nat [lemma, in Coq.Strings.Byte]
of_N_None_iff [lemma, in Coq.Strings.Byte]
of_to_N [lemma, in Coq.Strings.Byte]
of_N [definition, in Coq.Strings.Byte]
of_nat_None_iff [lemma, in Coq.Strings.Byte]
of_to_nat [lemma, in Coq.Strings.Byte]
of_nat [definition, in Coq.Strings.Byte]
of_iff [lemma, in Coq.Numbers.HexadecimalQ]
of_inj [lemma, in Coq.Numbers.HexadecimalQ]
of_hexadecimal_dnorm [lemma, in Coq.Numbers.HexadecimalQ]
of_to [lemma, in Coq.Numbers.HexadecimalQ]
of_IQmake_to_hexadecimal' [lemma, in Coq.Numbers.HexadecimalQ]
of_IQmake_to_hexadecimal [lemma, in Coq.Numbers.HexadecimalQ]
of_iff [lemma, in Coq.Numbers.DecimalR]
of_inj [lemma, in Coq.Numbers.DecimalR]
of_decimal_dnorm [lemma, in Coq.Numbers.DecimalR]
of_to [lemma, in Coq.Numbers.DecimalR]
of_IQmake_to_decimal [lemma, in Coq.Numbers.DecimalR]
of_nat_to_nat_eq [lemma, in Coq.micromega.ZifyInst]
of_Z_spec [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
of_pos_rec_spec [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
of_to_Z [axiom, in Coq.Numbers.Cyclic.Int63.Uint63]
of_Z [definition, in Coq.Numbers.Cyclic.Int63.Uint63]
of_pos [definition, in Coq.Numbers.Cyclic.Int63.Uint63]
of_pos_rec [definition, in Coq.Numbers.Cyclic.Int63.Uint63]
of_pos_spec [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]
of_Z_cmod [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]
of_Z_spec [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]
of_to_Z [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]
of_list [definition, in Coq.Vectors.VectorDef]
of_Bvector [definition, in Coq.Strings.ByteVector]
of_string [definition, in Coq.Strings.ByteVector]
of_uint63_spec [axiom, in Coq.Floats.FloatAxioms]
of_number [definition, in Coq.QArith.QArith_base]
of_hexadecimal [definition, in Coq.QArith.QArith_base]
of_decimal [definition, in Coq.QArith.QArith_base]
OLE [constructor, in Coq.Structures.OrdersTac]
olift [abbreviation, in Coq.ssr.ssrfun]
olift_comp [lemma, in Coq.ssr.ssrfun]
OLT [constructor, in Coq.Structures.OrdersTac]
omap [abbreviation, in Coq.ssr.ssrfun]
omapEapp [lemma, in Coq.ssr.ssrfun]
omapEbind [lemma, in Coq.ssr.ssrfun]
omap_comp [lemma, in Coq.ssr.ssrfun]
OmegaLemmas [library]
OMEGA1 [lemma, in Coq.omega.OmegaLemmas]
OMEGA10 [lemma, in Coq.omega.OmegaLemmas]
OMEGA11 [lemma, in Coq.omega.OmegaLemmas]
OMEGA12 [lemma, in Coq.omega.OmegaLemmas]
OMEGA13 [lemma, in Coq.omega.OmegaLemmas]
OMEGA14 [lemma, in Coq.omega.OmegaLemmas]
OMEGA15 [lemma, in Coq.omega.OmegaLemmas]
OMEGA16 [lemma, in Coq.omega.OmegaLemmas]
OMEGA17 [lemma, in Coq.omega.OmegaLemmas]
OMEGA18 [lemma, in Coq.omega.OmegaLemmas]
OMEGA19 [lemma, in Coq.omega.OmegaLemmas]
OMEGA2 [lemma, in Coq.omega.OmegaLemmas]
OMEGA20 [lemma, in Coq.omega.OmegaLemmas]
OMEGA3 [lemma, in Coq.omega.OmegaLemmas]
OMEGA4 [lemma, in Coq.omega.OmegaLemmas]
OMEGA5 [lemma, in Coq.omega.OmegaLemmas]
OMEGA6 [lemma, in Coq.omega.OmegaLemmas]
OMEGA7 [lemma, in Coq.omega.OmegaLemmas]
OMEGA8 [lemma, in Coq.omega.OmegaLemmas]
OMEGA9 [lemma, in Coq.omega.OmegaLemmas]
OmniscientFunctionalChoice [abbreviation, in Coq.Logic.ChoiceFacts]
OmniscientFunctionalChoice_on [definition, in Coq.Logic.ChoiceFacts]
OmniscientRelationalChoice [abbreviation, in Coq.Logic.ChoiceFacts]
OmniscientRelationalChoice_on [definition, in Coq.Logic.ChoiceFacts]
omniscient_fun_choice_imp_fun_choice [lemma, in Coq.Logic.ChoiceFacts]
omniscient_fun_choice_imp_small_drinker [lemma, in Coq.Logic.ChoiceFacts]
On [definition, in Coq.Numbers.Cyclic.Int31.Int31]
one [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
one [definition, in Coq.Floats.PrimFloat]
one [definition, in Coq.Init.Nat]
one [projection, in Coq.setoid_ring.Algebra_syntax]
One [record, in Coq.setoid_ring.Algebra_syntax]
one [constructor, in Coq.setoid_ring.Algebra_syntax]
One [inductive, in Coq.setoid_ring.Algebra_syntax]
one [definition, in Coq.Strings.Ascii]
OneTwo [module, in Coq.Numbers.NatInt.NZAxioms]
OneTwoNotation [module, in Coq.Numbers.NatInt.NZAxioms]
1 [notation, in Coq.Numbers.NatInt.NZAxioms]
2 [notation, in Coq.Numbers.NatInt.NZAxioms]
OneTwo' [module, in Coq.Numbers.NatInt.NZAxioms]
OneTwo.one [axiom, in Coq.Numbers.NatInt.NZAxioms]
OneTwo.two [axiom, in Coq.Numbers.NatInt.NZAxioms]
one_IZR_r_R1 [lemma, in Coq.Reals.RIneq]
one_IZR_lt1 [lemma, in Coq.Reals.RIneq]
one_notation [instance, in Coq.setoid_ring.Ncring]
onPhantom [definition, in Coq.ssr.ssrbool]
onS_can_in [lemma, in Coq.ssr.ssrbool]
onS_can [lemma, in Coq.ssr.ssrbool]
onT_bij [lemma, in Coq.ssr.ssrbool]
onW_can_in [lemma, in Coq.ssr.ssrbool]
onW_can [lemma, in Coq.ssr.ssrbool]
onW_bij [lemma, in Coq.ssr.ssrbool]
on_can_inj [lemma, in Coq.ssr.ssrbool]
on1lS [lemma, in Coq.ssr.ssrbool]
on1lS_in [lemma, in Coq.ssr.ssrbool]
on1lT [lemma, in Coq.ssr.ssrbool]
on1lW [lemma, in Coq.ssr.ssrbool]
on1lW_in [lemma, in Coq.ssr.ssrbool]
on1S [lemma, in Coq.ssr.ssrbool]
on1S_in [lemma, in Coq.ssr.ssrbool]
on1T [lemma, in Coq.ssr.ssrbool]
on1W [lemma, in Coq.ssr.ssrbool]
on1W_in [lemma, in Coq.ssr.ssrbool]
on2S [lemma, in Coq.ssr.ssrbool]
on2S_in [lemma, in Coq.ssr.ssrbool]
on2T [lemma, in Coq.ssr.ssrbool]
on2W [lemma, in Coq.ssr.ssrbool]
on2W_in [lemma, in Coq.ssr.ssrbool]
OpAdd [definition, in Coq.micromega.RingMicromega]
OpAdd_sound [lemma, in Coq.micromega.RingMicromega]
open_set_P6 [lemma, in Coq.Reals.Rtopology]
open_set_P5 [lemma, in Coq.Reals.Rtopology]
open_set_P4 [lemma, in Coq.Reals.Rtopology]
open_set_P3 [lemma, in Coq.Reals.Rtopology]
open_set_P2 [lemma, in Coq.Reals.Rtopology]
open_set_P1 [lemma, in Coq.Reals.Rtopology]
open_set [definition, in Coq.Reals.Rtopology]
open_interval [definition, in Coq.Reals.RiemannInt_SF]
OpEq [constructor, in Coq.micromega.RingMicromega]
OperationProperties [section, in Coq.ssr.ssrfun]
OperationProperties.R [variable, in Coq.ssr.ssrfun]
OperationProperties.S [variable, in Coq.ssr.ssrfun]
OperationProperties.SopSisS [section, in Coq.ssr.ssrfun]
OperationProperties.SopSisT [section, in Coq.ssr.ssrfun]
OperationProperties.SopTisR [section, in Coq.ssr.ssrfun]
OperationProperties.SopTisS [section, in Coq.ssr.ssrfun]
OperationProperties.SopTisT [section, in Coq.ssr.ssrfun]
OperationProperties.T [variable, in Coq.ssr.ssrfun]
Operators_Properties [library]
OpGe [constructor, in Coq.micromega.RingMicromega]
OpGt [constructor, in Coq.micromega.RingMicromega]
OpLe [constructor, in Coq.micromega.RingMicromega]
OpLt [constructor, in Coq.micromega.RingMicromega]
OpMult [definition, in Coq.micromega.RingMicromega]
OpMult_sound [lemma, in Coq.micromega.RingMicromega]
OpNEq [constructor, in Coq.micromega.RingMicromega]
opp [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
opp [definition, in Coq.Init.Decimal]
opp [axiom, in Coq.Floats.PrimFloat]
opp [definition, in Coq.Init.Hexadecimal]
Opp [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
opp [definition, in Coq.Numbers.Cyclic.Int63.Uint63]
oppc [definition, in Coq.Numbers.Cyclic.Int63.Uint63]
oppcarry [definition, in Coq.Numbers.Cyclic.Int63.Uint63]
oppcarry_spec [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
OppCstNotation [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
- 2 [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
- 1 [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
oppc_spec [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
OppNotation [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
- _ [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
opposite [projection, in Coq.setoid_ring.Algebra_syntax]
Opposite [record, in Coq.setoid_ring.Algebra_syntax]
opposite [constructor, in Coq.setoid_ring.Algebra_syntax]
Opposite [inductive, in Coq.setoid_ring.Algebra_syntax]
opp_carry [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
opp_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
opp_fct [definition, in Coq.Reals.Ranalysis1]
opp_IZR [lemma, in Coq.Reals.RIneq]
opp_inject_Z [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
opp_inject_Q [lemma, in Coq.Reals.Cauchy.ConstructiveCauchyReals]
opp_notation [instance, in Coq.setoid_ring.Ncring]
opp_to_Z_opp [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
opp_spec [lemma, in Coq.Numbers.Cyclic.Int63.Uint63]
opp_seq [definition, in Coq.Reals.SeqProp]
opp_of_Z [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]
opp_spec [lemma, in Coq.Numbers.Cyclic.Int63.Sint63]
opp_spec [axiom, in Coq.Floats.FloatAxioms]
Opp' [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
Opp.opp [axiom, in Coq.Numbers.Integer.Abstract.ZAxioms]
opp31 [definition, in Coq.Numbers.Cyclic.Int31.Int31]
Ops [module, in Coq.MSets.MSetInterface]
Ops [module, in Coq.MSets.MSetWeakList]
Ops [module, in Coq.MSets.MSetList]
Ops [module, in Coq.MSets.MSetAVL]
Ops [module, in Coq.MSets.MSetRBT]
Ops [module, in Coq.MSets.MSetGenTree]
Ops.add [definition, in Coq.MSets.MSetWeakList]
Ops.add [definition, in Coq.MSets.MSetList]
Ops.add [definition, in Coq.MSets.MSetAVL]
Ops.add [definition, in Coq.MSets.MSetRBT]
Ops.append [definition, in Coq.MSets.MSetRBT]
Ops.assert_false [definition, in Coq.MSets.MSetAVL]
Ops.bal [definition, in Coq.MSets.MSetAVL]
Ops.Bk [abbreviation, in Coq.MSets.MSetRBT]
Ops.bogus [definition, in Coq.MSets.MSetRBT]
Ops.cardinal [definition, in Coq.MSets.MSetWeakList]
Ops.cardinal [definition, in Coq.MSets.MSetList]
Ops.cardinal [definition, in Coq.MSets.MSetGenTree]
Ops.choose [definition, in Coq.MSets.MSetWeakList]
Ops.choose [definition, in Coq.MSets.MSetList]
Ops.choose [definition, in Coq.MSets.MSetGenTree]
Ops.compare [definition, in Coq.MSets.MSetList]
Ops.compare [definition, in Coq.MSets.MSetGenTree]
Ops.compare_height [definition, in Coq.MSets.MSetRBT]
Ops.compare_end [definition, in Coq.MSets.MSetGenTree]
Ops.compare_cont [definition, in Coq.MSets.MSetGenTree]
Ops.compare_more [definition, in Coq.MSets.MSetGenTree]
Ops.concat [definition, in Coq.MSets.MSetAVL]
Ops.cons [definition, in Coq.MSets.MSetGenTree]
Ops.create [definition, in Coq.MSets.MSetAVL]
Ops.del [definition, in Coq.MSets.MSetRBT]
Ops.delmin [definition, in Coq.MSets.MSetRBT]
Ops.diff [definition, in Coq.MSets.MSetWeakList]
Ops.diff [definition, in Coq.MSets.MSetList]
Ops.diff [definition, in Coq.MSets.MSetAVL]
Ops.diff [definition, in Coq.MSets.MSetRBT]
Ops.diff_list [definition, in Coq.MSets.MSetRBT]
Ops.elements [definition, in Coq.MSets.MSetWeakList]
Ops.elements [definition, in Coq.MSets.MSetList]
Ops.elements [definition, in Coq.MSets.MSetGenTree]
Ops.elements_aux [definition, in Coq.MSets.MSetGenTree]
Ops.elt [definition, in Coq.MSets.MSetWeakList]
Ops.elt [definition, in Coq.MSets.MSetList]
Ops.elt [definition, in Coq.MSets.MSetGenTree]
Ops.empty [definition, in Coq.MSets.MSetWeakList]
Ops.empty [definition, in Coq.MSets.MSetList]
Ops.empty [definition, in Coq.MSets.MSetGenTree]
Ops.End [constructor, in Coq.MSets.MSetGenTree]
Ops.enumeration [inductive, in Coq.MSets.MSetGenTree]
Ops.equal [definition, in Coq.MSets.MSetWeakList]
Ops.equal [definition, in Coq.MSets.MSetList]
Ops.equal [definition, in Coq.MSets.MSetGenTree]
Ops.exists_ [definition, in Coq.MSets.MSetWeakList]
Ops.exists_ [definition, in Coq.MSets.MSetList]
Ops.exists_ [definition, in Coq.MSets.MSetGenTree]
Ops.filter [definition, in Coq.MSets.MSetWeakList]
Ops.filter [definition, in Coq.MSets.MSetList]
Ops.filter [definition, in Coq.MSets.MSetAVL]
Ops.filter [definition, in Coq.MSets.MSetRBT]
Ops.filter_aux [definition, in Coq.MSets.MSetRBT]
Ops.fold [definition, in Coq.MSets.MSetWeakList]
Ops.fold [definition, in Coq.MSets.MSetList]
Ops.fold [definition, in Coq.MSets.MSetGenTree]
Ops.for_all [definition, in Coq.MSets.MSetWeakList]
Ops.for_all [definition, in Coq.MSets.MSetList]
Ops.for_all [definition, in Coq.MSets.MSetGenTree]
Ops.height [definition, in Coq.MSets.MSetAVL]
Ops.ins [definition, in Coq.MSets.MSetRBT]
Ops.int [abbreviation, in Coq.MSets.MSetAVL]
Ops.inter [definition, in Coq.MSets.MSetWeakList]
Ops.inter [definition, in Coq.MSets.MSetList]
Ops.inter [definition, in Coq.MSets.MSetAVL]
Ops.inter [definition, in Coq.MSets.MSetRBT]
Ops.inter_list [definition, in Coq.MSets.MSetRBT]
Ops.is_empty [definition, in Coq.MSets.MSetWeakList]
Ops.is_empty [definition, in Coq.MSets.MSetList]
Ops.is_empty [definition, in Coq.MSets.MSetGenTree]
Ops.join [definition, in Coq.MSets.MSetAVL]
Ops.lbal [definition, in Coq.MSets.MSetRBT]
Ops.lbalS [definition, in Coq.MSets.MSetRBT]
Ops.Leaf [constructor, in Coq.MSets.MSetGenTree]
Ops.linear_diff [definition, in Coq.MSets.MSetRBT]
Ops.linear_inter [definition, in Coq.MSets.MSetRBT]
Ops.linear_union [definition, in Coq.MSets.MSetRBT]
Ops.makeBlack [definition, in Coq.MSets.MSetRBT]
Ops.makeRed [definition, in Coq.MSets.MSetRBT]
Ops.maxdepth [definition, in Coq.MSets.MSetGenTree]
Ops.max_elt [definition, in Coq.MSets.MSetList]
Ops.max_elt [definition, in Coq.MSets.MSetGenTree]
Ops.mem [definition, in Coq.MSets.MSetWeakList]
Ops.mem [definition, in Coq.MSets.MSetList]
Ops.mem [definition, in Coq.MSets.MSetGenTree]
Ops.merge [definition, in Coq.MSets.MSetAVL]
Ops.mindepth [definition, in Coq.MSets.MSetGenTree]
Ops.min_elt [definition, in Coq.MSets.MSetList]
Ops.min_elt [definition, in Coq.MSets.MSetGenTree]
Ops.More [constructor, in Coq.MSets.MSetGenTree]
Ops.Node [constructor, in Coq.MSets.MSetGenTree]
Ops.partition [definition, in Coq.MSets.MSetWeakList]
Ops.partition [definition, in Coq.MSets.MSetList]
Ops.partition [definition, in Coq.MSets.MSetAVL]
Ops.partition [definition, in Coq.MSets.MSetRBT]
Ops.partition_aux [definition, in Coq.MSets.MSetRBT]
Ops.plength [definition, in Coq.MSets.MSetRBT]
Ops.plength_aux [definition, in Coq.MSets.MSetRBT]
Ops.rbal [definition, in Coq.MSets.MSetRBT]
Ops.rbalS [definition, in Coq.MSets.MSetRBT]
Ops.rbal' [definition, in Coq.MSets.MSetRBT]
Ops.Rd [abbreviation, in Coq.MSets.MSetRBT]
Ops.remove [definition, in Coq.MSets.MSetWeakList]
Ops.remove [definition, in Coq.MSets.MSetList]
Ops.remove [definition, in Coq.MSets.MSetAVL]
Ops.remove [definition, in Coq.MSets.MSetRBT]
Ops.remove_min [definition, in Coq.MSets.MSetAVL]
Ops.remove_min [definition, in Coq.MSets.MSetRBT]
Ops.rev_elements [definition, in Coq.MSets.MSetGenTree]
Ops.rev_elements_aux [definition, in Coq.MSets.MSetGenTree]
Ops.singleton [definition, in Coq.MSets.MSetWeakList]
Ops.singleton [definition, in Coq.MSets.MSetList]
Ops.singleton [definition, in Coq.MSets.MSetAVL]
Ops.singleton [definition, in Coq.MSets.MSetRBT]
Ops.skip_black [definition, in Coq.MSets.MSetRBT]
Ops.skip_red [definition, in Coq.MSets.MSetRBT]
Ops.split [definition, in Coq.MSets.MSetAVL]
Ops.subset [definition, in Coq.MSets.MSetWeakList]
Ops.subset [definition, in Coq.MSets.MSetList]
Ops.subset [definition, in Coq.MSets.MSetGenTree]
Ops.subsetl [definition, in Coq.MSets.MSetGenTree]
Ops.subsetr [definition, in Coq.MSets.MSetGenTree]
Ops.t [definition, in Coq.MSets.MSetWeakList]
Ops.t [definition, in Coq.MSets.MSetList]
Ops.t [definition, in Coq.MSets.MSetAVL]
Ops.t [definition, in Coq.MSets.MSetRBT]
Ops.tree [inductive, in Coq.MSets.MSetGenTree]
Ops.treeify [definition, in Coq.MSets.MSetRBT]
Ops.treeify_aux [definition, in Coq.MSets.MSetRBT]
Ops.treeify_cont [definition, in Coq.MSets.MSetRBT]
Ops.treeify_one [definition, in Coq.MSets.MSetRBT]
Ops.treeify_zero [definition, in Coq.MSets.MSetRBT]
Ops.treeify_t [abbreviation, in Coq.MSets.MSetRBT]
Ops.triple [record, in Coq.MSets.MSetAVL]
Ops.t_right [projection, in Coq.MSets.MSetAVL]
Ops.t_in [projection, in Coq.MSets.MSetAVL]
Ops.t_left [projection, in Coq.MSets.MSetAVL]
Ops.union [definition, in Coq.MSets.MSetWeakList]
Ops.union [definition, in Coq.MSets.MSetList]
Ops.union [definition, in Coq.MSets.MSetAVL]
Ops.union [definition, in Coq.MSets.MSetRBT]
Ops.union_list [definition, in Coq.MSets.MSetRBT]
<< _ , _ , _ >> [notation, in Coq.MSets.MSetAVL]
Option [module, in Coq.ssr.ssrfun]
option [inductive, in Coq.Init.Datatypes]
Option [library]
OptionTheory [section, in Coq.ssr.ssrfun]
OptionTheory.aT [variable, in Coq.ssr.ssrfun]
OptionTheory.f [variable, in Coq.ssr.ssrfun]
OptionTheory.g [variable, in Coq.ssr.ssrfun]
OptionTheory.rT [variable, in Coq.ssr.ssrfun]
OptionTheory.sT [variable, in Coq.ssr.ssrfun]
option_map [definition, in Coq.Init.Datatypes]
option_sind [definition, in Coq.Init.Datatypes]
option_rec [definition, in Coq.Init.Datatypes]
option_ind [definition, in Coq.Init.Datatypes]
option_rect [definition, in Coq.Init.Datatypes]
Option.apply [definition, in Coq.ssr.ssrfun]
Option.bind [definition, in Coq.ssr.ssrfun]
Option.default [definition, in Coq.ssr.ssrfun]
Option.lift [definition, in Coq.ssr.ssrfun]
Option.map [definition, in Coq.ssr.ssrfun]
op_iff [projection, in Coq.micromega.ZifyClasses]
Op_b2z [instance, in Coq.micromega.ZifyBool]
Op_b2n [instance, in Coq.micromega.ZifyBool]
Op_nat_ltb [instance, in Coq.micromega.ZifyBool]
Op_nat_leb [instance, in Coq.micromega.ZifyBool]
Op_nat_eqb [instance, in Coq.micromega.ZifyBool]
Op_Pos_ltb [instance, in Coq.micromega.ZifyBool]
Op_Pos_leb [instance, in Coq.micromega.ZifyBool]
Op_Pos_eqb [instance, in Coq.micromega.ZifyBool]
Op_Nltb [instance, in Coq.micromega.ZifyBool]
Op_Nleb [instance, in Coq.micromega.ZifyBool]
Op_Neqb [instance, in Coq.micromega.ZifyBool]
Op_Zgtb [instance, in Coq.micromega.ZifyBool]
Op_Zltb [instance, in Coq.micromega.ZifyBool]
Op_Zgeb [instance, in Coq.micromega.ZifyBool]
Op_Zleb [instance, in Coq.micromega.ZifyBool]
Op_Zeqb [instance, in Coq.micromega.ZifyBool]
Op_false [instance, in Coq.micromega.ZifyBool]
Op_true [instance, in Coq.micromega.ZifyBool]
Op_eq_bool [instance, in Coq.micromega.ZifyBool]
Op_negb [instance, in Coq.micromega.ZifyBool]
Op_eqb [instance, in Coq.micromega.ZifyBool]
Op_xorb [instance, in Coq.micromega.ZifyBool]
Op_implb [instance, in Coq.micromega.ZifyBool]
Op_orb [instance, in Coq.micromega.ZifyBool]
Op_andb [instance, in Coq.micromega.ZifyBool]
Op_pow [instance, in Coq.micromega.ZifyNat]
Op_div [instance, in Coq.micromega.ZifyNat]
Op_mod [instance, in Coq.micromega.ZifyNat]
Op_abs [instance, in Coq.micromega.ZifySint63]
Op_is_zero [instance, in Coq.micromega.ZifySint63]
Op_to_Z [instance, in Coq.micromega.ZifySint63]
Op_of_Z [instance, in Coq.micromega.ZifySint63]
Op_div [instance, in Coq.micromega.ZifySint63]
Op_asr [instance, in Coq.micromega.ZifySint63]
Op_mod [instance, in Coq.micromega.ZifySint63]
Op_mul [instance, in Coq.micromega.ZifySint63]
Op_pred [instance, in Coq.micromega.ZifySint63]
Op_succ [instance, in Coq.micromega.ZifySint63]
Op_opp [instance, in Coq.micromega.ZifySint63]
Op_sub [instance, in Coq.micromega.ZifySint63]
Op_add [instance, in Coq.micromega.ZifySint63]
Op_eq [instance, in Coq.micromega.ZifySint63]
Op_eqb [instance, in Coq.micromega.ZifySint63]
Op_leb [instance, in Coq.micromega.ZifySint63]
Op_ltb [instance, in Coq.micromega.ZifySint63]
Op_wB [instance, in Coq.micromega.ZifySint63]
Op_size [instance, in Coq.micromega.ZifySint63]
Op_digits [instance, in Coq.micromega.ZifySint63]
Op_min_int [instance, in Coq.micromega.ZifySint63]
Op_max_int [instance, in Coq.micromega.ZifySint63]
Op_Gt [instance, in Coq.micromega.ZifyComparison]
Op_Lt [instance, in Coq.micromega.ZifyComparison]
Op_Eq [instance, in Coq.micromega.ZifyComparison]
Op_eq_comparison [instance, in Coq.micromega.ZifyComparison]
Op_is_even [instance, in Coq.micromega.ZifyUint63]
Op_is_zero [instance, in Coq.micromega.ZifyUint63]
Op_to_Z [instance, in Coq.micromega.ZifyUint63]
Op_of_Z [instance, in Coq.micromega.ZifyUint63]
Op_bit [instance, in Coq.micromega.ZifyUint63]
Op_div [instance, in Coq.micromega.ZifyUint63]
Op_lxor [instance, in Coq.micromega.ZifyUint63]
Op_land [instance, in Coq.micromega.ZifyUint63]
Op_lor [instance, in Coq.micromega.ZifyUint63]
Op_lsl [instance, in Coq.micromega.ZifyUint63]
Op_lsr [instance, in Coq.micromega.ZifyUint63]
Op_addcarry [instance, in Coq.micromega.ZifyUint63]
Op_subcarry [instance, in Coq.micromega.ZifyUint63]
Op_mod [instance, in Coq.micromega.ZifyUint63]
Op_gcd [instance, in Coq.micromega.ZifyUint63]
Op_mul [instance, in Coq.micromega.ZifyUint63]
Op_pred [instance, in Coq.micromega.ZifyUint63]
Op_succ [instance, in Coq.micromega.ZifyUint63]
Op_oppcarry [instance, in Coq.micromega.ZifyUint63]
Op_opp [instance, in Coq.micromega.ZifyUint63]
Op_sub [instance, in Coq.micromega.ZifyUint63]
Op_add [instance, in Coq.micromega.ZifyUint63]
Op_eq [instance, in Coq.micromega.ZifyUint63]
Op_eqb [instance, in Coq.micromega.ZifyUint63]
Op_leb [instance, in Coq.micromega.ZifyUint63]
Op_ltb [instance, in Coq.micromega.ZifyUint63]
Op_wB [instance, in Coq.micromega.ZifyUint63]
Op_size [instance, in Coq.micromega.ZifyUint63]
Op_digits [instance, in Coq.micromega.ZifyUint63]
Op_max_int [instance, in Coq.micromega.ZifyUint63]
op_rotate [lemma, in Coq.Sets.Permut]
Op_N_pow [instance, in Coq.micromega.ZifyN]
Op_N_mod [instance, in Coq.micromega.ZifyN]
Op_N_div [instance, in Coq.micromega.ZifyN]
Op_Z_to_pos [instance, in Coq.micromega.ZifyInst]
Op_Z_to_nat [instance, in Coq.micromega.ZifyInst]
Op_Z_quot2 [instance, in Coq.micromega.ZifyInst]
Op_Z_div2 [instance, in Coq.micromega.ZifyInst]
Op_Z_square [instance, in Coq.micromega.ZifyInst]
Op_Z_succ_double [instance, in Coq.micromega.ZifyInst]
Op_Z_pred_double [instance, in Coq.micromega.ZifyInst]
Op_Z_double [instance, in Coq.micromega.ZifyInst]
Op_Z_pow_pos [instance, in Coq.micromega.ZifyInst]
Op_Z_pow [instance, in Coq.micromega.ZifyInst]
Op_Z_sgn [instance, in Coq.micromega.ZifyInst]
Op_Z_abs [instance, in Coq.micromega.ZifyInst]
Op_Z_opp [instance, in Coq.micromega.ZifyInst]
Op_Z_pred [instance, in Coq.micromega.ZifyInst]
Op_Z_succ [instance, in Coq.micromega.ZifyInst]
Op_Z_quot [instance, in Coq.micromega.ZifyInst]
Op_Z_rem [instance, in Coq.micromega.ZifyInst]
Op_Z_mod [instance, in Coq.micromega.ZifyInst]
Op_Z_div [instance, in Coq.micromega.ZifyInst]
Op_Z_sub [instance, in Coq.micromega.ZifyInst]
Op_Z_mul [instance, in Coq.micromega.ZifyInst]
Op_Z_max [instance, in Coq.micromega.ZifyInst]
Op_Z_min [instance, in Coq.micromega.ZifyInst]
Op_Z_add [instance, in Coq.micromega.ZifyInst]
Op_Z_Z0 [instance, in Coq.micromega.ZifyInst]
Op_eqZ [instance, in Coq.micromega.ZifyInst]
Op_Z_le [instance, in Coq.micromega.ZifyInst]
Op_Z_gt [instance, in Coq.micromega.ZifyInst]
Op_Z_lt [instance, in Coq.micromega.ZifyInst]
Op_Z_ge [instance, in Coq.micromega.ZifyInst]
Op_N_square [instance, in Coq.micromega.ZifyInst]
Op_N_pow [instance, in Coq.micromega.ZifyInst]
Op_N_div2 [instance, in Coq.micromega.ZifyInst]
Op_N_succ_pos [instance, in Coq.micromega.ZifyInst]
Op_N_double [instance, in Coq.micromega.ZifyInst]
Op_N_succ_double [instance, in Coq.micromega.ZifyInst]
Op_N_succ [instance, in Coq.micromega.ZifyInst]
Op_N_pred [instance, in Coq.micromega.ZifyInst]
Op_N_mod [instance, in Coq.micromega.ZifyInst]
Op_N_div [instance, in Coq.micromega.ZifyInst]
Op_N_sub [instance, in Coq.micromega.ZifyInst]
Op_N_mul [instance, in Coq.micromega.ZifyInst]
Op_N_max [instance, in Coq.micromega.ZifyInst]
Op_N_min [instance, in Coq.micromega.ZifyInst]
Op_N_add [instance, in Coq.micromega.ZifyInst]
Op_N_pos [instance, in Coq.micromega.ZifyInst]
Op_Z_abs_N [instance, in Coq.micromega.ZifyInst]
Op_N_of_nat [instance, in Coq.micromega.ZifyInst]
Op_N_Npos [instance, in Coq.micromega.ZifyInst]
Op_N_N0 [instance, in Coq.micromega.ZifyInst]
Op_eq_N [instance, in Coq.micromega.ZifyInst]
Op_N_le [instance, in Coq.micromega.ZifyInst]
Op_N_gt [instance, in Coq.micromega.ZifyInst]
Op_N_lt [instance, in Coq.micromega.ZifyInst]
Op_N_ge [instance, in Coq.micromega.ZifyInst]
Op_Z_of_nat [instance, in Coq.micromega.ZifyInst]
Op_xH [instance, in Coq.micromega.ZifyInst]
Op_xI [instance, in Coq.micromega.ZifyInst]
Op_xO [instance, in Coq.micromega.ZifyInst]
Op_Pos_Ndouble [instance, in Coq.micromega.ZifyInst]
Op_Pos_Nsucc_double [instance, in Coq.micromega.ZifyInst]
Op_pos_square [instance, in Coq.micromega.ZifyInst]
Op_pos_pow [instance, in Coq.micromega.ZifyInst]
Op_pos_max [instance, in Coq.micromega.ZifyInst]
Op_pos_min [instance, in Coq.micromega.ZifyInst]
Op_pos_mul [instance, in Coq.micromega.ZifyInst]
Op_pos_sub [instance, in Coq.micromega.ZifyInst]
Op_pos_add_carry [instance, in Coq.micromega.ZifyInst]
Op_pos_add [instance, in Coq.micromega.ZifyInst]
Op_pos_of_nat [instance, in Coq.micromega.ZifyInst]
Op_pos_of_succ_nat [instance, in Coq.micromega.ZifyInst]
Op_pos_predN [instance, in Coq.micromega.ZifyInst]
Op_pos_pred [instance, in Coq.micromega.ZifyInst]
Op_pos_pred_double [instance, in Coq.micromega.ZifyInst]
Op_pos_succ [instance, in Coq.micromega.ZifyInst]
Op_Z_pos [instance, in Coq.micromega.ZifyInst]
Op_Z_neg [instance, in Coq.micromega.ZifyInst]
Op_Z_to_N [instance, in Coq.micromega.ZifyInst]
Op_Z_of_N [instance, in Coq.micromega.ZifyInst]
Op_eq_pos [instance, in Coq.micromega.ZifyInst]
Op_pos_le [instance, in Coq.micromega.ZifyInst]
Op_pos_gt [instance, in Coq.micromega.ZifyInst]
Op_pos_lt [instance, in Coq.micromega.ZifyInst]
Op_pos_ge [instance, in Coq.micromega.ZifyInst]
Op_N_to_nat [instance, in Coq.micromega.ZifyInst]
Op_pos_to_nat [instance, in Coq.micromega.ZifyInst]
Op_Z_abs_nat [instance, in Coq.micromega.ZifyInst]
Op_O [instance, in Coq.micromega.ZifyInst]
Op_S [instance, in Coq.micromega.ZifyInst]
Op_pred [instance, in Coq.micromega.ZifyInst]
Op_max [instance, in Coq.micromega.ZifyInst]
Op_min [instance, in Coq.micromega.ZifyInst]
Op_mul [instance, in Coq.micromega.ZifyInst]
Op_sub [instance, in Coq.micromega.ZifyInst]
Op_plus [instance, in Coq.micromega.ZifyInst]
Op_Nat_eq [instance, in Coq.micromega.ZifyInst]
Op_eq_nat [instance, in Coq.micromega.ZifyInst]
Op_Nat_le [instance, in Coq.micromega.ZifyInst]
Op_le [instance, in Coq.micromega.ZifyInst]
Op_gt [instance, in Coq.micromega.ZifyInst]
Op_Nat_lt [instance, in Coq.micromega.ZifyInst]
Op_lt [instance, in Coq.micromega.ZifyInst]
Op_ge [instance, in Coq.micromega.ZifyInst]
Op1 [inductive, in Coq.micromega.RingMicromega]
Op1_sind [definition, in Coq.micromega.RingMicromega]
Op1_rec [definition, in Coq.micromega.RingMicromega]
Op1_ind [definition, in Coq.micromega.RingMicromega]
Op1_rect [definition, in Coq.micromega.RingMicromega]
Op2 [inductive, in Coq.micromega.RingMicromega]
Op2_sind [definition, in Coq.micromega.RingMicromega]
Op2_rec [definition, in Coq.micromega.RingMicromega]
Op2_ind [definition, in Coq.micromega.RingMicromega]
Op2_rect [definition, in Coq.micromega.RingMicromega]
or [inductive, in Coq.Init.Logic]
OR [constructor, in Coq.micromega.Tauto]
orb [definition, in Coq.Init.Datatypes]
orbA [lemma, in Coq.ssr.ssrbool]
orbAC [lemma, in Coq.ssr.ssrbool]
orbACA [lemma, in Coq.ssr.ssrbool]
orbb [lemma, in Coq.ssr.ssrbool]
orbC [lemma, in Coq.ssr.ssrbool]
orbCA [lemma, in Coq.ssr.ssrbool]
orbF [lemma, in Coq.ssr.ssrbool]
orbK [lemma, in Coq.ssr.ssrbool]
orbN [lemma, in Coq.ssr.ssrbool]
orbT [lemma, in Coq.ssr.ssrbool]
orb_id2r [lemma, in Coq.ssr.ssrbool]
orb_id2l [lemma, in Coq.ssr.ssrbool]
orb_idr [lemma, in Coq.ssr.ssrbool]
orb_idl [lemma, in Coq.ssr.ssrbool]
orb_andr [lemma, in Coq.ssr.ssrbool]
orb_andl [lemma, in Coq.ssr.ssrbool]
orb_lazy_alt [lemma, in Coq.Bool.Bool]
orb_prop_intro [lemma, in Coq.Bool.Bool]
orb_prop2 [abbreviation, in Coq.Bool.Bool]
orb_prop_elim [lemma, in Coq.Bool.Bool]
orb_andb_distrib_l [lemma, in Coq.Bool.Bool]
orb_andb_distrib_r [lemma, in Coq.Bool.Bool]
orb_assoc [lemma, in Coq.Bool.Bool]
orb_comm [lemma, in Coq.Bool.Bool]
orb_neg_b [abbreviation, in Coq.Bool.Bool]
orb_negb_l [lemma, in Coq.Bool.Bool]
orb_negb_r [lemma, in Coq.Bool.Bool]
orb_false_b [abbreviation, in Coq.Bool.Bool]
orb_b_false [abbreviation, in Coq.Bool.Bool]
orb_false_l [lemma, in Coq.Bool.Bool]
orb_false_r [lemma, in Coq.Bool.Bool]
orb_true_b [abbreviation, in Coq.Bool.Bool]
orb_b_true [abbreviation, in Coq.Bool.Bool]
orb_true_l [lemma, in Coq.Bool.Bool]
orb_true_r [lemma, in Coq.Bool.Bool]
orb_diag [lemma, in Coq.Bool.Bool]
orb_false_elim [lemma, in Coq.Bool.Bool]
orb_false_intro [lemma, in Coq.Bool.Bool]
orb_true_intro [lemma, in Coq.Bool.Bool]
orb_prop [lemma, in Coq.Bool.Bool]
orb_true_elim [lemma, in Coq.Bool.Bool]
orb_false_iff [lemma, in Coq.Bool.Bool]
orb_true_iff [lemma, in Coq.Bool.Bool]
ord [inductive, in Coq.Structures.OrdersTac]
Order [inductive, in Coq.Sets.Relations_1]
order [record, in Coq.Relations.Relation_Definitions]
OrderedRing [library]
OrderedRingSyntax [module, in Coq.micromega.OrderedRing]
OrderedType [module, in Coq.Structures.Orders]
OrderedType [module, in Coq.Structures.OrderedType]
OrderedType [library]
OrderedTypeAlt [module, in Coq.Structures.OrdersAlt]
OrderedTypeAlt [module, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt [library]
OrderedTypeAlt.compare [axiom, in Coq.Structures.OrdersAlt]
OrderedTypeAlt.compare [axiom, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt.compare_trans [axiom, in Coq.Structures.OrdersAlt]
OrderedTypeAlt.compare_sym [axiom, in Coq.Structures.OrdersAlt]
OrderedTypeAlt.compare_trans [axiom, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt.compare_sym [axiom, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt.t [axiom, in Coq.Structures.OrdersAlt]
OrderedTypeAlt.t [axiom, in Coq.Structures.OrderedTypeAlt]
_ ?= _ [notation, in Coq.Structures.OrdersAlt]
_ ?= _ [notation, in Coq.Structures.OrderedTypeAlt]
OrderedTypeEx [library]
OrderedTypeFacts [module, in Coq.Structures.OrderedType]
OrderedTypeFacts [module, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.compare_ge_iff [abbreviation, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.compare_le_iff [abbreviation, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.elim_compare_gt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.elim_compare_lt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.elim_compare_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eqb [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.eqb [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eqb_alt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eqb_compat [instance, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eqb_alt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_dec [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_not_gt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_not_lt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_neq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_le [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_lt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_equiv [instance, in Coq.Structures.OrderedType]
OrderedTypeFacts.eq_dec [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_trans [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_sym [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eq_refl [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.ForNotations [section, in Coq.Structures.OrderedType]
OrderedTypeFacts.gt_not_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.if_eq_dec [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.In [abbreviation, in Coq.Structures.OrderedType]
OrderedTypeFacts.Inf [abbreviation, in Coq.Structures.OrderedType]
OrderedTypeFacts.Inf_alt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.Inf_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.Inf_lt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.In_Inf [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.In_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO [module, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.eq_equiv [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.le_lteq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.lt_total [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.lt_compat [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.IsTO.lt_strorder [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.le_antisym [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.le_trans [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.le_neq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.le_lt_trans [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.le_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.ListIn_Inf [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.ListIn_In [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_dec [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_not_gt [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_le [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_le_trans [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_total [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_compat [instance, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_strorder [instance, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_antirefl [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.lt_dec [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.lt_irrefl [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.lt_trans [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.neq_sym [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.neq_eq [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.NoDup [abbreviation, in Coq.Structures.OrderedType]
OrderedTypeFacts.OrderTac [module, in Coq.Structures.OrderedType]
OrderedTypeFacts.OrderTac [module, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.Sort [abbreviation, in Coq.Structures.OrderedType]
OrderedTypeFacts.Sort_NoDup [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.Sort_Inf_In [lemma, in Coq.Structures.OrderedType]
OrderedTypeFacts.TO [module, in Coq.Structures.OrderedType]
OrderedTypeFacts.TO.eq [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.TO.le [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.TO.lt [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.TO.t [definition, in Coq.Structures.OrderedType]
_ ?= _ (order) [notation, in Coq.Structures.OrdersFacts]
_ <= _ (order) [notation, in Coq.Structures.OrdersFacts]
OrderedTypeFull [module, in Coq.Structures.Orders]
OrderedTypeFullFacts [module, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.compare_ge_iff [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.compare_le_iff [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.eq_is_le_ge [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_or_gt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_not_gt_iff [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_antisym [instance, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_order [instance, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_preorder [instance, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.le_compat [instance, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.lt_or_ge [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.lt_not_ge_iff [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFullFacts.OrderTac [module, in Coq.Structures.OrdersFacts]
OrderedTypeFull' [module, in Coq.Structures.Orders]
OrderedTypeLists [module, in Coq.Structures.OrdersLists]
OrderedTypeLists.In [abbreviation, in Coq.Structures.OrdersLists]
OrderedTypeLists.Inf [abbreviation, in Coq.Structures.OrdersLists]
OrderedTypeLists.Inf_alt [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.Inf_eq [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.Inf_lt [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.In_Inf [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.In_eq [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.ListIn_Inf [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.ListIn_In [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.NoDup [abbreviation, in Coq.Structures.OrdersLists]
OrderedTypeLists.Sort [abbreviation, in Coq.Structures.OrdersLists]
OrderedTypeLists.Sort_NoDup [lemma, in Coq.Structures.OrdersLists]
OrderedTypeLists.Sort_Inf_In [lemma, in Coq.Structures.OrdersLists]
OrderedTypeOrig [module, in Coq.Structures.OrdersAlt]
OrderedTypeRev [module, in Coq.Structures.OrdersFacts]
OrderedTypeRev.compare [definition, in Coq.Structures.OrdersFacts]
OrderedTypeRev.compare_spec [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeRev.eq [definition, in Coq.Structures.OrdersFacts]
OrderedTypeRev.eq_dec [definition, in Coq.Structures.OrdersFacts]
OrderedTypeRev.eq_equiv [instance, in Coq.Structures.OrdersFacts]
OrderedTypeRev.le [definition, in Coq.Structures.OrdersFacts]
OrderedTypeRev.le_lteq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeRev.lt [definition, in Coq.Structures.OrdersFacts]
OrderedTypeRev.lt_compat [instance, in Coq.Structures.OrdersFacts]
OrderedTypeRev.lt_strorder [instance, in Coq.Structures.OrdersFacts]
OrderedTypeRev.t [definition, in Coq.Structures.OrdersFacts]
OrderedTypeTest [module, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_is_nlt_ngt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_not_gt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_not_lt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_neq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_le [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.eq_lt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.gt_not_eq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_neq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_antisym [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_trans [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_lt_trans [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.le_eq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_not_gt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_le [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_le_trans [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_eq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.lt_not_eq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.MO [module, in Coq.Structures.OrdersFacts]
OrderedTypeTest.neq_sym [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeTest.neq_eq [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeWithLeibniz [module, in Coq.MSets.MSetList]
OrderedTypeWithLeibniz.eq_leibniz [axiom, in Coq.MSets.MSetList]
OrderedType_to_Alt.compare_trans [lemma, in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt.compare_sym [lemma, in Coq.Structures.OrderedTypeAlt]
_ ?= _ [notation, in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt.compare [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt.t [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt.MO [module, in Coq.Structures.OrderedTypeAlt]
OrderedType_to_Alt [module, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_dec [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.compare [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.lt_not_eq [lemma, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.lt_trans [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_trans [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_sym [lemma, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq_refl [lemma, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.lt [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.eq [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt.t [definition, in Coq.Structures.OrderedTypeAlt]
OrderedType_from_Alt [module, in Coq.Structures.OrderedTypeAlt]
OrderedType' [module, in Coq.Structures.Orders]
OrderedType.eq_dec [axiom, in Coq.Structures.OrderedType]
ordered_Rlist [definition, in Coq.Reals.RList]
OrderFacts [module, in Coq.Structures.OrdersTac]
OrderFacts.eq_neq [lemma, in Coq.Structures.OrdersTac]
OrderFacts.eq_le [definition, in Coq.Structures.OrdersTac]
OrderFacts.eq_lt [definition, in Coq.Structures.OrdersTac]
OrderFacts.eq_trans [definition, in Coq.Structures.OrdersTac]
OrderFacts.eq_sym [lemma, in Coq.Structures.OrdersTac]
OrderFacts.eq_refl [lemma, in Coq.Structures.OrdersTac]
OrderFacts.interp_ord [definition, in Coq.Structures.OrdersTac]
OrderFacts.le_neq_lt [lemma, in Coq.Structures.OrdersTac]
OrderFacts.le_eq [definition, in Coq.Structures.OrdersTac]
OrderFacts.le_lt_trans [definition, in Coq.Structures.OrdersTac]
OrderFacts.le_trans [definition, in Coq.Structures.OrdersTac]
OrderFacts.le_antisym [lemma, in Coq.Structures.OrdersTac]
OrderFacts.le_refl [lemma, in Coq.Structures.OrdersTac]
OrderFacts.lt_eq [definition, in Coq.Structures.OrdersTac]
OrderFacts.lt_le_trans [definition, in Coq.Structures.OrdersTac]
OrderFacts.lt_trans [definition, in Coq.Structures.OrdersTac]
OrderFacts.lt_irrefl [lemma, in Coq.Structures.OrdersTac]
OrderFacts.neq_eq [lemma, in Coq.Structures.OrdersTac]
OrderFacts.neq_sym [lemma, in Coq.Structures.OrdersTac]
OrderFacts.not_gt_le [lemma, in Coq.Structures.OrdersTac]
OrderFacts.not_ge_lt [lemma, in Coq.Structures.OrdersTac]
OrderFacts.not_neq_eq [lemma, in Coq.Structures.OrdersTac]
OrderFacts.trans [lemma, in Coq.Structures.OrdersTac]
# [notation, in Coq.Structures.OrdersTac]
OrderFunctions [module, in Coq.Structures.Orders]
OrderFunctions' [module, in Coq.Structures.Orders]
Orders [library]
OrdersAlt [library]
OrdersEx [library]
OrdersFacts [library]
OrdersLists [library]
OrdersTac [library]
Order_sind [definition, in Coq.Sets.Relations_1]
Order_rec [definition, in Coq.Sets.Relations_1]
Order_ind [definition, in Coq.Sets.Relations_1]
Order_rect [definition, in Coq.Sets.Relations_1]
OrdProperties [module, in Coq.MSets.MSetProperties]
OrdProperties [module, in Coq.FSets.FMapFacts]
OrdProperties [module, in Coq.FSets.FSetProperties]
OrdProperties.Above [definition, in Coq.MSets.MSetProperties]
OrdProperties.Above [definition, in Coq.FSets.FMapFacts]
OrdProperties.Above [definition, in Coq.FSets.FSetProperties]
OrdProperties.Add [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.add_fold [lemma, in Coq.MSets.MSetProperties]
OrdProperties.add_fold [lemma, in Coq.FSets.FSetProperties]
OrdProperties.Below [definition, in Coq.MSets.MSetProperties]
OrdProperties.Below [definition, in Coq.FSets.FMapFacts]
OrdProperties.Below [definition, in Coq.FSets.FSetProperties]
OrdProperties.cardinal [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.choose_equal [lemma, in Coq.MSets.MSetProperties]
OrdProperties.choose_equal [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_Add_Below [lemma, in Coq.MSets.MSetProperties]
OrdProperties.elements_Add_Above [lemma, in Coq.MSets.MSetProperties]
OrdProperties.elements_Add [lemma, in Coq.MSets.MSetProperties]
OrdProperties.elements_split [lemma, in Coq.MSets.MSetProperties]
OrdProperties.elements_ge [definition, in Coq.MSets.MSetProperties]
OrdProperties.elements_lt [definition, in Coq.MSets.MSetProperties]
OrdProperties.elements_Equal_eqlistA [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Below [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Above [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_Add [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_split [lemma, in Coq.FSets.FMapFacts]
OrdProperties.elements_ge [definition, in Coq.FSets.FMapFacts]
OrdProperties.elements_lt [definition, in Coq.FSets.FMapFacts]
OrdProperties.elements_Add_Below [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_Add_Above [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_Add [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_split [lemma, in Coq.FSets.FSetProperties]
OrdProperties.elements_ge [definition, in Coq.FSets.FSetProperties]
OrdProperties.elements_lt [definition, in Coq.FSets.FSetProperties]
OrdProperties.Elt [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Elements [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.elt [variable, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Fold_properties [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Induction_Principles [section, in Coq.FSets.FMapFacts]
OrdProperties.Elt.Min_Max_Elt [section, in Coq.FSets.FMapFacts]
OrdProperties.eqk [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.eqke [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.Equal [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.FoldOpt [section, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt [section, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.A [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.A [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.Comp [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.Comp [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.eqA [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.eqA [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.f [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.f [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.st [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.st [variable, in Coq.FSets.FSetProperties]
OrdProperties.fold_equal [lemma, in Coq.MSets.MSetProperties]
OrdProperties.fold_4 [lemma, in Coq.MSets.MSetProperties]
OrdProperties.fold_3 [lemma, in Coq.MSets.MSetProperties]
OrdProperties.fold_Add_Below [lemma, in Coq.FSets.FMapFacts]
OrdProperties.fold_Add_Above [lemma, in Coq.FSets.FMapFacts]
OrdProperties.fold_Equal [lemma, in Coq.FSets.FMapFacts]
OrdProperties.fold_equal [lemma, in Coq.FSets.FSetProperties]
OrdProperties.fold_4 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.fold_3 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.gtb [definition, in Coq.MSets.MSetProperties]
OrdProperties.gtb [definition, in Coq.FSets.FMapFacts]
OrdProperties.gtb [definition, in Coq.FSets.FSetProperties]
OrdProperties.gtb_compat [instance, in Coq.MSets.MSetProperties]
OrdProperties.gtb_1 [lemma, in Coq.MSets.MSetProperties]
OrdProperties.gtb_compat [lemma, in Coq.FSets.FMapFacts]
OrdProperties.gtb_1 [lemma, in Coq.FSets.FMapFacts]
OrdProperties.gtb_compat [lemma, in Coq.FSets.FSetProperties]
OrdProperties.gtb_1 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.leb [definition, in Coq.MSets.MSetProperties]
OrdProperties.leb [definition, in Coq.FSets.FMapFacts]
OrdProperties.leb [definition, in Coq.FSets.FSetProperties]
OrdProperties.leb_compat [instance, in Coq.MSets.MSetProperties]
OrdProperties.leb_1 [lemma, in Coq.MSets.MSetProperties]
OrdProperties.leb_compat [lemma, in Coq.FSets.FMapFacts]
OrdProperties.leb_1 [lemma, in Coq.FSets.FMapFacts]
OrdProperties.leb_compat [lemma, in Coq.FSets.FSetProperties]
OrdProperties.leb_1 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.ltk [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.map_induction_min [lemma, in Coq.FSets.FMapFacts]
OrdProperties.map_induction_max [lemma, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_Empty [lemma, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_MapsTo [lemma, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_Above [lemma, in Coq.FSets.FMapFacts]
OrdProperties.max_elt [definition, in Coq.FSets.FMapFacts]
OrdProperties.max_elt_aux [definition, in Coq.FSets.FMapFacts]
OrdProperties.ME [module, in Coq.MSets.MSetProperties]
OrdProperties.ME [module, in Coq.FSets.FMapFacts]
OrdProperties.ME [module, in Coq.FSets.FSetProperties]
OrdProperties.min_elt_Empty [lemma, in Coq.FSets.FMapFacts]
OrdProperties.min_elt_MapsTo [lemma, in Coq.FSets.FMapFacts]
OrdProperties.min_elt_Below [lemma, in Coq.FSets.FMapFacts]
OrdProperties.min_elt [definition, in Coq.FSets.FMapFacts]
OrdProperties.ML [module, in Coq.MSets.MSetProperties]
OrdProperties.O [module, in Coq.FSets.FMapFacts]
OrdProperties.P [module, in Coq.MSets.MSetProperties]
OrdProperties.P [module, in Coq.FSets.FMapFacts]
OrdProperties.P [module, in Coq.FSets.FSetProperties]
OrdProperties.remove_fold_2 [lemma, in Coq.MSets.MSetProperties]
OrdProperties.remove_fold_2 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.set_induction_min [lemma, in Coq.MSets.MSetProperties]
OrdProperties.set_induction_max [lemma, in Coq.MSets.MSetProperties]
OrdProperties.set_induction_min [lemma, in Coq.FSets.FSetProperties]
OrdProperties.set_induction_max [lemma, in Coq.FSets.FSetProperties]
OrdProperties.sort_equivlistA_eqlistA [lemma, in Coq.MSets.MSetProperties]
OrdProperties.sort_equivlistA_eqlistA [lemma, in Coq.FSets.FMapFacts]
OrdProperties.sort_equivlistA_eqlistA [lemma, in Coq.FSets.FSetProperties]
ord_sind [definition, in Coq.Structures.OrdersTac]
ord_rec [definition, in Coq.Structures.OrdersTac]
ord_ind [definition, in Coq.Structures.OrdersTac]
ord_rect [definition, in Coq.Structures.OrdersTac]
ord_antisym [projection, in Coq.Relations.Relation_Definitions]
ord_trans [projection, in Coq.Relations.Relation_Definitions]
ord_refl [projection, in Coq.Relations.Relation_Definitions]
orFb [lemma, in Coq.ssr.ssrbool]
orKb [lemma, in Coq.ssr.ssrbool]
orNb [lemma, in Coq.ssr.ssrbool]
orP [lemma, in Coq.ssr.ssrbool]
orPP [lemma, in Coq.ssr.ssrbool]
orTb [lemma, in Coq.ssr.ssrbool]
or_not_r_iff_2 [lemma, in Coq.Logic.Decidable]
or_not_r_iff_1 [lemma, in Coq.Logic.Decidable]
or_not_l_iff_2 [lemma, in Coq.Logic.Decidable]
or_not_l_iff_1 [lemma, in Coq.Logic.Decidable]
or_morph [lemma, in Coq.micromega.ZifyClasses]
or_iff_morphism [instance, in Coq.Classes.Morphisms_Prop]
or_impl_morphism [instance, in Coq.Classes.Morphisms_Prop]
or_not_and [lemma, in Coq.Logic.Classical_Prop]
or_to_imply [lemma, in Coq.Logic.Classical_Prop]
or_assoc [lemma, in Coq.Init.Logic]
or_comm [lemma, in Coq.Init.Logic]
or_cancel_r [lemma, in Coq.Init.Logic]
or_cancel_l [lemma, in Coq.Init.Logic]
or_iff_compat_r [lemma, in Coq.Init.Logic]
or_iff_compat_l [lemma, in Coq.Init.Logic]
or_sind [definition, in Coq.Init.Logic]
or_ind [definition, in Coq.Init.Logic]
or_intror [constructor, in Coq.Init.Logic]
or_introl [constructor, in Coq.Init.Logic]
or_indd [definition, in Coq.Logic.ClassicalFacts]
or_elim_redr [definition, in Coq.Logic.ClassicalFacts]
or_elim_redl [definition, in Coq.Logic.ClassicalFacts]
or_cnf_opt_correct [lemma, in Coq.micromega.Tauto]
or_cnf_correct [lemma, in Coq.micromega.Tauto]
or_clause_cnf_correct [lemma, in Coq.micromega.Tauto]
or_clause_correct [lemma, in Coq.micromega.Tauto]
or_is_X_inv [lemma, in Coq.micromega.Tauto]
or_cnf_opt_cnf_ff_r [lemma, in Coq.micromega.Tauto]
or_cnf_opt_cnf_ff [lemma, in Coq.micromega.Tauto]
or_is_X [definition, in Coq.micromega.Tauto]
or_cnf_opt [definition, in Coq.micromega.Tauto]
or_cnf [definition, in Coq.micromega.Tauto]
or_clause_cnf [definition, in Coq.micromega.Tauto]
or_clause [definition, in Coq.micromega.Tauto]
or3 [inductive, in Coq.ssr.ssrbool]
or3P [lemma, in Coq.ssr.ssrbool]
or3_sind [definition, in Coq.ssr.ssrbool]
or3_ind [definition, in Coq.ssr.ssrbool]
Or31 [constructor, in Coq.ssr.ssrbool]
Or32 [constructor, in Coq.ssr.ssrbool]
Or33 [constructor, in Coq.ssr.ssrbool]
or4 [inductive, in Coq.ssr.ssrbool]
or4P [lemma, in Coq.ssr.ssrbool]
or4_sind [definition, in Coq.ssr.ssrbool]
or4_ind [definition, in Coq.ssr.ssrbool]
Or41 [constructor, in Coq.ssr.ssrbool]
Or42 [constructor, in Coq.ssr.ssrbool]
Or43 [constructor, in Coq.ssr.ssrbool]
Or44 [constructor, in Coq.ssr.ssrbool]
OTF_to_TTLB.t [definition, in Coq.Structures.Orders]
OTF_to_TTLB.leb_trans [lemma, in Coq.Structures.Orders]
OTF_to_TTLB.leb_total [lemma, in Coq.Structures.Orders]
OTF_to_TTLB.leb_le [lemma, in Coq.Structures.Orders]
OTF_to_TTLB.leb [definition, in Coq.Structures.Orders]
OTF_to_TTLB [module, in Coq.Structures.Orders]
OTF_to_TotalOrder [module, in Coq.Structures.Orders]
OTF_LtIsTotal.lt_total [lemma, in Coq.Structures.Orders]
OTF_LtIsTotal [module, in Coq.Structures.Orders]
OTF_to_OrderTac.TO [module, in Coq.Structures.OrdersTac]
OTF_to_OrderTac [module, in Coq.Structures.OrdersTac]
other_definitions [section, in Coq.Lists.ListSet]
OT_to_Full.le_lteq [lemma, in Coq.Structures.Orders]
OT_to_Full.le [definition, in Coq.Structures.Orders]
OT_to_Full [module, in Coq.Structures.Orders]
OT_as_DT [module, in Coq.Structures.DecidableTypeEx]
OT_as_DT [module, in Coq.Structures.OrdersEx]
OT_to_Alt.compare_trans [lemma, in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_Gt [lemma, in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_Lt [lemma, in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_Eq [lemma, in Coq.Structures.OrdersAlt]
OT_to_Alt.compare_sym [lemma, in Coq.Structures.OrdersAlt]
_ ?= _ [notation, in Coq.Structures.OrdersAlt]
OT_to_Alt.compare [definition, in Coq.Structures.OrdersAlt]
OT_to_Alt.t [definition, in Coq.Structures.OrdersAlt]
OT_to_Alt [module, in Coq.Structures.OrdersAlt]
OT_from_Alt.eq_dec [definition, in Coq.Structures.OrdersAlt]
OT_from_Alt.compare_spec [lemma, in Coq.Structures.OrdersAlt]
OT_from_Alt.compare [definition, in Coq.Structures.OrdersAlt]
OT_from_Alt.lt_compat [instance, in Coq.Structures.OrdersAlt]
OT_from_Alt.eq_lt [lemma, in Coq.Structures.OrdersAlt]
OT_from_Alt.lt_eq [lemma, in Coq.Structures.OrdersAlt]
OT_from_Alt.lt_strorder [instance, in Coq.Structures.OrdersAlt]
OT_from_Alt.eq_equiv [instance, in Coq.Structures.OrdersAlt]
OT_from_Alt.lt [definition, in Coq.Structures.OrdersAlt]
OT_from_Alt.eq [definition, in Coq.Structures.OrdersAlt]
OT_from_Alt.t [definition, in Coq.Structures.OrdersAlt]
OT_from_Alt [module, in Coq.Structures.OrdersAlt]
OT_to_OrderTac.OTF [module, in Coq.Structures.OrdersTac]
OT_to_OrderTac [module, in Coq.Structures.OrdersTac]
over [definition, in Coq.ssr.ssreflect]
O_witness [definition, in Coq.Logic.ConstructiveEpsilon]
O_S [lemma, in Coq.Init.Peano]
O_or_S [lemma, in Coq.Arith.Peano_dec]
| 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 | (26611 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 | (1022 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 | (806 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 | (1548 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 | (595 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 | (12054 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 | (959 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 | (629 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 | (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 | (505 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 | (912 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 | (1508 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 | (5124 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) |