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 | (18795 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 | (548 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 | (203 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 | (67 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 | (8930 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 | (338 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 | (422 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 | (644 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 | (1237 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 | (209 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 | (2932 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 | (703 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 | (699 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 | (1456 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 | (407 entries)

## O

O [constructor, in Coq.Init.Datatypes]
obligation [definition, in Coq.Program.Tactics]
ObsoletePmultNat [section, in Coq.PArith.Pnat]
odd [definition, in Coq.Numbers.Natural.Peano.NPeano]
Odd [definition, in Coq.Numbers.Natural.Peano.NPeano]
odd [inductive, in Coq.Arith.Even]
odd_even_lem [lemma, in Coq.Arith.Mult]
odd_bitwise [lemma, in Coq.Numbers.Natural.Peano.NPeano]
Odd_equiv [lemma, in Coq.Numbers.Natural.Peano.NPeano]
odd_spec [lemma, in Coq.Numbers.Natural.Peano.NPeano]
odd_mult_inv_r [lemma, in Coq.Arith.Even]
odd_mult_inv_l [lemma, in Coq.Arith.Even]
odd_mult [lemma, in Coq.Arith.Even]
odd_plus_odd_inv_r [lemma, in Coq.Arith.Even]
odd_plus_odd_inv_l [lemma, in Coq.Arith.Even]
odd_plus_even_inv_r [lemma, in Coq.Arith.Even]
odd_plus_even_inv_l [lemma, in Coq.Arith.Even]
odd_even_plus [lemma, in Coq.Arith.Even]
odd_plus_r [lemma, in Coq.Arith.Even]
odd_plus_l [lemma, in Coq.Arith.Even]
odd_plus_split [lemma, in Coq.Arith.Even]
odd_S [constructor, in Coq.Arith.Even]
odd_S2n [lemma, in Coq.Arith.Div2]
odd_double [lemma, in Coq.Arith.Div2]
odd_div2 [lemma, in Coq.Arith.Div2]
OEQ [constructor, in Coq.Structures.OrdersTac]
of_list [definition, in Coq.Vectors.VectorDef]
of_pos [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
of_nat_to_nat_inv [lemma, in Coq.Vectors.Fin]
of_nat_lt [definition, in Coq.Vectors.Fin]
of_nat [definition, in Coq.Vectors.Fin]
OLE [constructor, in Coq.Structures.OrdersTac]
OLT [constructor, in Coq.Structures.OrdersTac]
Omega [lemma, in Coq.Logic.Hurkens]
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.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]
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]
Operators_Properties [library]
opp [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
Opp [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
OppCstNotation [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
- 2 [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
- 1 [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
OppNotation [module, in Coq.Numbers.Integer.Abstract.ZAxioms]
- _ [notation, in Coq.Numbers.Integer.Abstract.ZAxioms]
opp_seq [definition, in Coq.Reals.SeqProp]
opp_fct [definition, in Coq.Reals.Ranalysis1]
opp_IZR [lemma, in Coq.Reals.RIneq]
opp_carry [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
opp_c [definition, in Coq.Numbers.Cyclic.ZModulo.ZModulo]
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.MSetRBT]
Ops [module, in Coq.MSets.MSetGenTree]
Ops [module, in Coq.MSets.MSetWeakList]
Ops [module, in Coq.MSets.MSetList]
Ops [module, in Coq.MSets.MSetAVL]
Ops.add [definition, in Coq.MSets.MSetRBT]
Ops.add [definition, in Coq.MSets.MSetWeakList]
Ops.add [definition, in Coq.MSets.MSetList]
Ops.add [definition, in Coq.MSets.MSetAVL]
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.MSetGenTree]
Ops.cardinal [definition, in Coq.MSets.MSetWeakList]
Ops.cardinal [definition, in Coq.MSets.MSetList]
Ops.choose [definition, in Coq.MSets.MSetGenTree]
Ops.choose [definition, in Coq.MSets.MSetWeakList]
Ops.choose [definition, in Coq.MSets.MSetList]
Ops.compare [definition, in Coq.MSets.MSetGenTree]
Ops.compare [definition, in Coq.MSets.MSetList]
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.MSetRBT]
Ops.diff [definition, in Coq.MSets.MSetWeakList]
Ops.diff [definition, in Coq.MSets.MSetList]
Ops.diff [definition, in Coq.MSets.MSetAVL]
Ops.diff_list [definition, in Coq.MSets.MSetRBT]
Ops.elements [definition, in Coq.MSets.MSetGenTree]
Ops.elements [definition, in Coq.MSets.MSetWeakList]
Ops.elements [definition, in Coq.MSets.MSetList]
Ops.elements_aux [definition, in Coq.MSets.MSetGenTree]
Ops.elt [definition, in Coq.MSets.MSetGenTree]
Ops.elt [definition, in Coq.MSets.MSetWeakList]
Ops.elt [definition, in Coq.MSets.MSetList]
Ops.empty [definition, in Coq.MSets.MSetGenTree]
Ops.empty [definition, in Coq.MSets.MSetWeakList]
Ops.empty [definition, in Coq.MSets.MSetList]
Ops.End [constructor, in Coq.MSets.MSetGenTree]
Ops.enumeration [inductive, in Coq.MSets.MSetGenTree]
Ops.equal [definition, in Coq.MSets.MSetGenTree]
Ops.equal [definition, in Coq.MSets.MSetWeakList]
Ops.equal [definition, in Coq.MSets.MSetList]
Ops.exists_ [definition, in Coq.MSets.MSetGenTree]
Ops.exists_ [definition, in Coq.MSets.MSetWeakList]
Ops.exists_ [definition, in Coq.MSets.MSetList]
Ops.filter [definition, in Coq.MSets.MSetRBT]
Ops.filter [definition, in Coq.MSets.MSetWeakList]
Ops.filter [definition, in Coq.MSets.MSetList]
Ops.filter [definition, in Coq.MSets.MSetAVL]
Ops.filter_aux [definition, in Coq.MSets.MSetRBT]
Ops.fold [definition, in Coq.MSets.MSetGenTree]
Ops.fold [definition, in Coq.MSets.MSetWeakList]
Ops.fold [definition, in Coq.MSets.MSetList]
Ops.for_all [definition, in Coq.MSets.MSetGenTree]
Ops.for_all [definition, in Coq.MSets.MSetWeakList]
Ops.for_all [definition, in Coq.MSets.MSetList]
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.MSetRBT]
Ops.inter [definition, in Coq.MSets.MSetWeakList]
Ops.inter [definition, in Coq.MSets.MSetList]
Ops.inter [definition, in Coq.MSets.MSetAVL]
Ops.inter_list [definition, in Coq.MSets.MSetRBT]
Ops.is_empty [definition, in Coq.MSets.MSetGenTree]
Ops.is_empty [definition, in Coq.MSets.MSetWeakList]
Ops.is_empty [definition, in Coq.MSets.MSetList]
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.MSetGenTree]
Ops.max_elt [definition, in Coq.MSets.MSetList]
Ops.mem [definition, in Coq.MSets.MSetGenTree]
Ops.mem [definition, in Coq.MSets.MSetWeakList]
Ops.mem [definition, in Coq.MSets.MSetList]
Ops.merge [definition, in Coq.MSets.MSetAVL]
Ops.mindepth [definition, in Coq.MSets.MSetGenTree]
Ops.min_elt [definition, in Coq.MSets.MSetGenTree]
Ops.min_elt [definition, in Coq.MSets.MSetList]
Ops.mktriple [constructor, in Coq.MSets.MSetAVL]
Ops.More [constructor, in Coq.MSets.MSetGenTree]
Ops.Node [constructor, in Coq.MSets.MSetGenTree]
Ops.partition [definition, in Coq.MSets.MSetRBT]
Ops.partition [definition, in Coq.MSets.MSetWeakList]
Ops.partition [definition, in Coq.MSets.MSetList]
Ops.partition [definition, in Coq.MSets.MSetAVL]
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.MSetRBT]
Ops.remove [definition, in Coq.MSets.MSetWeakList]
Ops.remove [definition, in Coq.MSets.MSetList]
Ops.remove [definition, in Coq.MSets.MSetAVL]
Ops.remove_min [definition, in Coq.MSets.MSetRBT]
Ops.remove_min [definition, in Coq.MSets.MSetAVL]
Ops.rev_elements [definition, in Coq.MSets.MSetGenTree]
Ops.rev_elements_aux [definition, in Coq.MSets.MSetGenTree]
Ops.singleton [definition, in Coq.MSets.MSetRBT]
Ops.singleton [definition, in Coq.MSets.MSetWeakList]
Ops.singleton [definition, in Coq.MSets.MSetList]
Ops.singleton [definition, in Coq.MSets.MSetAVL]
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.MSetGenTree]
Ops.subset [definition, in Coq.MSets.MSetWeakList]
Ops.subset [definition, in Coq.MSets.MSetList]
Ops.subsetl [definition, in Coq.MSets.MSetGenTree]
Ops.subsetr [definition, in Coq.MSets.MSetGenTree]
Ops.t [definition, in Coq.MSets.MSetRBT]
Ops.t [definition, in Coq.MSets.MSetWeakList]
Ops.t [definition, in Coq.MSets.MSetList]
Ops.t [definition, in Coq.MSets.MSetAVL]
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.MSetRBT]
Ops.union [definition, in Coq.MSets.MSetWeakList]
Ops.union [definition, in Coq.MSets.MSetList]
Ops.union [definition, in Coq.MSets.MSetAVL]
Ops.union_list [definition, in Coq.MSets.MSetRBT]
<< _ , _ , _ >> [notation, in Coq.MSets.MSetAVL]
option [inductive, in Coq.Init.Datatypes]
option_map [definition, in Coq.Init.Datatypes]
op_rotate [lemma, in Coq.Sets.Permut]
or [inductive, in Coq.Init.Logic]
orb [definition, in Coq.Init.Datatypes]
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_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]
OrderedType [module, in Coq.Structures.Orders]
OrderedType [module, in Coq.Structures.OrderedType]
OrderedType [library]
OrderedTypeAlt [module, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt [module, in Coq.Structures.OrdersAlt]
OrderedTypeAlt [library]
OrderedTypeAlt.compare [axiom, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt.compare [axiom, in Coq.Structures.OrdersAlt]
OrderedTypeAlt.compare_trans [axiom, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt.compare_sym [axiom, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt.compare_trans [axiom, in Coq.Structures.OrdersAlt]
OrderedTypeAlt.compare_sym [axiom, in Coq.Structures.OrdersAlt]
OrderedTypeAlt.t [axiom, in Coq.Structures.OrderedTypeAlt]
OrderedTypeAlt.t [axiom, in Coq.Structures.OrdersAlt]
_ ?= _ [notation, in Coq.Structures.OrderedTypeAlt]
_ ?= _ [notation, in Coq.Structures.OrdersAlt]
OrderedTypeEx [library]
OrderedTypeFacts [module, in Coq.Structures.OrdersFacts]
OrderedTypeFacts [module, in Coq.Structures.OrderedType]
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.OrdersFacts]
OrderedTypeFacts.eqb [definition, in Coq.Structures.OrderedType]
OrderedTypeFacts.eqb_compat [instance, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eqb_alt [lemma, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.eqb_alt [lemma, 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.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.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.OrdersFacts]
OrderedTypeFacts.lt_irrefl [definition, in Coq.Structures.OrdersFacts]
OrderedTypeFacts.lt_trans [definition, in Coq.Structures.OrdersFacts]
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.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.OrdersFacts]
OrderedTypeFacts.OrderTac [module, in Coq.Structures.OrderedType]
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.ForNotations [section, 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]
OrdProperties [module, in Coq.FSets.FSetProperties]
OrdProperties [module, in Coq.MSets.MSetProperties]
OrdProperties [module, in Coq.FSets.FMapFacts]
OrdProperties.Above [definition, in Coq.FSets.FSetProperties]
OrdProperties.Above [definition, in Coq.MSets.MSetProperties]
OrdProperties.Above [definition, in Coq.FSets.FMapFacts]
OrdProperties.Add [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.add_fold [lemma, in Coq.FSets.FSetProperties]
OrdProperties.add_fold [lemma, in Coq.MSets.MSetProperties]
OrdProperties.Below [definition, in Coq.FSets.FSetProperties]
OrdProperties.Below [definition, in Coq.MSets.MSetProperties]
OrdProperties.Below [definition, in Coq.FSets.FMapFacts]
OrdProperties.cardinal [abbreviation, in Coq.FSets.FMapFacts]
OrdProperties.choose_equal [lemma, in Coq.FSets.FSetProperties]
OrdProperties.choose_equal [lemma, in Coq.MSets.MSetProperties]
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.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.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.FSets.FSetProperties]
OrdProperties.FoldOpt [section, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.A [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.A [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.Comp [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.Comp [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.eqA [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.eqA [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.f [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.f [variable, in Coq.MSets.MSetProperties]
OrdProperties.FoldOpt.st [variable, in Coq.FSets.FSetProperties]
OrdProperties.FoldOpt.st [variable, in Coq.MSets.MSetProperties]
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.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.gtb [definition, in Coq.FSets.FSetProperties]
OrdProperties.gtb [definition, in Coq.MSets.MSetProperties]
OrdProperties.gtb [definition, in Coq.FSets.FMapFacts]
OrdProperties.gtb_compat [lemma, in Coq.FSets.FSetProperties]
OrdProperties.gtb_1 [lemma, 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.leb [definition, in Coq.FSets.FSetProperties]
OrdProperties.leb [definition, in Coq.MSets.MSetProperties]
OrdProperties.leb [definition, in Coq.FSets.FMapFacts]
OrdProperties.leb_compat [lemma, in Coq.FSets.FSetProperties]
OrdProperties.leb_1 [lemma, 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.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.FSets.FSetProperties]
OrdProperties.ME [module, in Coq.MSets.MSetProperties]
OrdProperties.ME [module, in Coq.FSets.FMapFacts]
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.FSets.FSetProperties]
OrdProperties.P [module, in Coq.MSets.MSetProperties]
OrdProperties.P [module, in Coq.FSets.FMapFacts]
OrdProperties.remove_fold_2 [lemma, in Coq.FSets.FSetProperties]
OrdProperties.remove_fold_2 [lemma, in Coq.MSets.MSetProperties]
OrdProperties.set_induction_min [lemma, in Coq.FSets.FSetProperties]
OrdProperties.set_induction_max [lemma, in Coq.FSets.FSetProperties]
OrdProperties.set_induction_min [lemma, in Coq.MSets.MSetProperties]
OrdProperties.set_induction_max [lemma, in Coq.MSets.MSetProperties]
OrdProperties.sort_equivlistA_eqlistA [lemma, in Coq.FSets.FSetProperties]
OrdProperties.sort_equivlistA_eqlistA [lemma, in Coq.MSets.MSetProperties]
OrdProperties.sort_equivlistA_eqlistA [lemma, in Coq.FSets.FMapFacts]
ord_antisym [projection, in Coq.Relations.Relation_Definitions]
ord_trans [projection, in Coq.Relations.Relation_Definitions]
ord_refl [projection, in Coq.Relations.Relation_Definitions]
or_not_and [lemma, in Coq.Logic.Classical_Prop]
or_to_imply [lemma, in Coq.Logic.Classical_Prop]
or_indd [definition, in Coq.Logic.ClassicalFacts]
or_elim_redr [definition, in Coq.Logic.ClassicalFacts]
or_elim_redl [definition, in Coq.Logic.ClassicalFacts]
or_iff_morphism [instance, in Coq.Classes.Morphisms_Prop]
or_impl_morphism [instance, in Coq.Classes.Morphisms_Prop]
or_iff_compat_r [lemma, in Coq.Init.Logic]
or_iff_compat_l [lemma, in Coq.Init.Logic]
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_intror [constructor, in Coq.Init.Logic]
or_introl [constructor, in Coq.Init.Logic]
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]
OTF_to_OrderTac.TO [module, in Coq.Structures.OrdersTac]
OTF_to_OrderTac [module, in Coq.Structures.OrdersTac]
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]
other_definitions [section, in Coq.Lists.ListSet]
OT_as_DT [module, in Coq.Structures.OrdersEx]
OT_to_OrderTac.OTF [module, in Coq.Structures.OrdersTac]
OT_to_OrderTac [module, in Coq.Structures.OrdersTac]
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_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]
O_or_S [lemma, in Coq.Arith.Peano_dec]
O_witness [definition, in Coq.Logic.ConstructiveEpsilon]
O_S [lemma, in Coq.Init.Peano]

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 | (18795 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 | (548 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 | (203 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 | (67 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 | (8930 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 | (338 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 | (422 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 | (644 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 | (1237 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 | (209 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 | (2932 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 | (703 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 | (699 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 | (1456 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 | (407 entries)