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 (224 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 (20 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 (15 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 (34 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 (92 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 (1 entry) 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 (28 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 (9 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 (25 entries)

# Global Index

## A

and_commutative [lemma, in CoursDeCoq.ex1]
and_commutative [lemma, in CoursDeCoq.ex1_auto]
Antisymmetric [definition, in CoursDeCoq.Relations_1]

## B

Bottom [inductive, in CoursDeCoq.podefs_1]
Bottom_definition [constructor, in CoursDeCoq.podefs_1]
Bounds [section, in CoursDeCoq.podefs_1]
Bounds.C [variable, in CoursDeCoq.podefs_1]
Bounds.D [variable, in CoursDeCoq.podefs_1]
Bounds.R [variable, in CoursDeCoq.podefs_1]
Bounds.U [variable, in CoursDeCoq.podefs_1]

## C

Carrier [definition, in CoursDeCoq.podefs]
Carrier_of [lemma, in CoursDeCoq.podefs]
Chain [definition, in CoursDeCoq.podefs_1]
coherent [definition, in CoursDeCoq.Relations_3]
coherent_symmetric [lemma, in CoursDeCoq.Relations_3_facts]
Compatible [definition, in CoursDeCoq.podefs_1]
Compatible_is_symmetric [lemma, in CoursDeCoq.Partial_order_facts]
Compatible_is_reflexive [lemma, in CoursDeCoq.Partial_order_facts]
Complement [definition, in CoursDeCoq.Relations_1_facts]
Complete [inductive, in CoursDeCoq.podefs_1]
Conditionally_complete [inductive, in CoursDeCoq.podefs_1]
Conditionally_complete_has_a_bottom [lemma, in CoursDeCoq.Partial_order_facts]
Confluent [definition, in CoursDeCoq.Relations_3]
confluent [definition, in CoursDeCoq.Relations_3]
contains [definition, in CoursDeCoq.Relations_1]
contains_is_preorder [lemma, in CoursDeCoq.Relations_1_facts]
Couple [inductive, in CoursDeCoq.Ensembles]
Couple_is_symmetric [lemma, in CoursDeCoq.Partial_order_facts]
Couple_included_in_carrier [lemma, in CoursDeCoq.Partial_order_facts]
Couple_r [constructor, in CoursDeCoq.Ensembles]
Couple_l [constructor, in CoursDeCoq.Ensembles]
Cpo [definition, in CoursDeCoq.podefs_1]

## D

Definition_of_Conditionally_complete [constructor, in CoursDeCoq.podefs_1]
Definition_of_Complete [constructor, in CoursDeCoq.podefs_1]
Definition_of_Directed [constructor, in CoursDeCoq.podefs_1]
Definition_of_PO [constructor, in CoursDeCoq.podefs]
Definition_of_PER [constructor, in CoursDeCoq.Relations_1]
Definition_of_equivalence [constructor, in CoursDeCoq.Relations_1]
Definition_of_order [constructor, in CoursDeCoq.Relations_1]
Definition_of_preorder [constructor, in CoursDeCoq.Relations_1]
Definition_of_Power_set [constructor, in CoursDeCoq.ps]
definition_of_noetherian [constructor, in CoursDeCoq.Relations_3]
Directed [inductive, in CoursDeCoq.podefs_1]
Disjoint [inductive, in CoursDeCoq.Ensembles]
Disjoint_intro [constructor, in CoursDeCoq.Ensembles]
drinker [library]
drinker's_theorem [lemma, in CoursDeCoq.drinker]

## E

Empty_set_has_lub [lemma, in CoursDeCoq.Partial_order_facts]
Empty_set_has_Upper_Bound [lemma, in CoursDeCoq.Partial_order_facts]
Empty_is_finite [constructor, in CoursDeCoq.Ensembles]
Empty_set [inductive, in CoursDeCoq.Ensembles]
Empty_set_zero [lemma, in CoursDeCoq.ps]
Empty_set_is_Bottom [lemma, in CoursDeCoq.ps]
Empty_set_minimal [lemma, in CoursDeCoq.ps]
Ensemble [definition, in CoursDeCoq.Ensembles]
Ensembles [section, in CoursDeCoq.Ensembles]
Ensembles [library]
Ensembles.U [variable, in CoursDeCoq.Ensembles]
Equivalence [inductive, in CoursDeCoq.Relations_1]
Equiv_from_order [lemma, in CoursDeCoq.Relations_1_facts]
Equiv_from_preorder [lemma, in CoursDeCoq.Relations_1_facts]
Extensionality_Ensembles [axiom, in CoursDeCoq.Ensembles]
ex1 [library]
ex1_auto [library]

## F

Fil [library]
Finite [inductive, in CoursDeCoq.Ensembles]
Finite_plus_one_is_finite [lemma, in CoursDeCoq.ps]
First_inductive_lemmas.D [variable, in CoursDeCoq.Fil]
First_inductive_lemmas.B [variable, in CoursDeCoq.Fil]
First_inductive_lemmas.U [variable, in CoursDeCoq.Fil]
First_inductive_lemmas [section, in CoursDeCoq.Fil]

## G

Glb [inductive, in CoursDeCoq.podefs_1]
Glb_definition [constructor, in CoursDeCoq.podefs_1]

## I

In [definition, in CoursDeCoq.Ensembles]
Included [definition, in CoursDeCoq.Ensembles]
Inclusion_is_transitive [lemma, in CoursDeCoq.ps]
Inclusion_is_an_order [lemma, in CoursDeCoq.ps]
Intersection [inductive, in CoursDeCoq.Ensembles]
Intersection_intro [constructor, in CoursDeCoq.Ensembles]
Intersection_is_Glb [lemma, in CoursDeCoq.ps]
Intersection_decreases_r [lemma, in CoursDeCoq.ps]
Intersection_decreases_l [lemma, in CoursDeCoq.ps]
Intersection_maximal [lemma, in CoursDeCoq.ps]
In_singleton [constructor, in CoursDeCoq.Ensembles]

## L

Lemmas_on_partial_orders.D [variable, in CoursDeCoq.Partial_order_facts]
Lemmas_on_partial_orders.B [variable, in CoursDeCoq.Partial_order_facts]
Lemmas_on_partial_orders.U [variable, in CoursDeCoq.Partial_order_facts]
Lemmas_on_partial_orders [section, in CoursDeCoq.Partial_order_facts]
Lemma1 [lemma, in CoursDeCoq.Relations_2_facts]
Locally_confluent [definition, in CoursDeCoq.Relations_3]
locally_confluent [definition, in CoursDeCoq.Relations_3]
Lower_Bound_definition [constructor, in CoursDeCoq.podefs_1]
Lower_Bound [inductive, in CoursDeCoq.podefs_1]
Lub [inductive, in CoursDeCoq.podefs_1]
Lub_definition [constructor, in CoursDeCoq.podefs_1]
Lub_is_in_Carrier [lemma, in CoursDeCoq.Partial_order_facts]

## M

mini_cases [lemma, in CoursDeCoq.ex1]
mini_cases [lemma, in CoursDeCoq.ex1_auto]
mp [lemma, in CoursDeCoq.ex1]
mp [lemma, in CoursDeCoq.ex1_auto]

## N

Newman [lemma, in CoursDeCoq.Relations_3_facts]
Noetherian [definition, in CoursDeCoq.Relations_3]
noetherian [inductive, in CoursDeCoq.Relations_3]
Noetherian_contains_Noetherian [lemma, in CoursDeCoq.Relations_3_facts]
Non_empty_intro [constructor, in CoursDeCoq.Ensembles]
Non_empty [inductive, in CoursDeCoq.Ensembles]
Non_disjoint_union [lemma, in CoursDeCoq.ps]
not_quite_classic [lemma, in CoursDeCoq.ex1]
not_not_converse [lemma, in CoursDeCoq.ex1]
not_not [lemma, in CoursDeCoq.ex1]
not_quite_classic [lemma, in CoursDeCoq.ex1_auto]
not_not_converse [lemma, in CoursDeCoq.ex1_auto]
not_not [lemma, in CoursDeCoq.ex1_auto]

## O

Order [inductive, in CoursDeCoq.Relations_1]
or_commutative [lemma, in CoursDeCoq.ex1]
or_commutative [lemma, in CoursDeCoq.ex1_auto]

## P

Pairs_are_enough [lemma, in CoursDeCoq.Fil]
Pairs_are_enough_finite_case [lemma, in CoursDeCoq.Fil]
Partial_orders.U [variable, in CoursDeCoq.podefs]
Partial_orders [section, in CoursDeCoq.podefs]
Partial_order_facts [library]
Peirce [lemma, in CoursDeCoq.ex1_auto]
PER [inductive, in CoursDeCoq.Relations_1]
PO [inductive, in CoursDeCoq.podefs]
podefs [library]
podefs_1 [library]
Power_set_PO [lemma, in CoursDeCoq.ps]
Power_set_non_empty [lemma, in CoursDeCoq.ps]
Power_set [inductive, in CoursDeCoq.ps]
Praeclarum [lemma, in CoursDeCoq.ex1]
Praeclarum [lemma, in CoursDeCoq.ex1_auto]
Preorder [inductive, in CoursDeCoq.Relations_1]
ps [library]

## R

Reflexive [definition, in CoursDeCoq.Relations_1]
Rel [definition, in CoursDeCoq.podefs]
Relation [definition, in CoursDeCoq.Relations_1]
Relations_1.R [variable, in CoursDeCoq.Relations_1]
Relations_1.U [variable, in CoursDeCoq.Relations_1]
Relations_1 [section, in CoursDeCoq.Relations_1]
Relations_2.R [variable, in CoursDeCoq.Relations_2]
Relations_2.U [variable, in CoursDeCoq.Relations_2]
Relations_2 [section, in CoursDeCoq.Relations_2]
Relations_3.R [variable, in CoursDeCoq.Relations_3]
Relations_3.U [variable, in CoursDeCoq.Relations_3]
Relations_3 [section, in CoursDeCoq.Relations_3]
Relations_2 [library]
Relations_3 [library]
Relations_1 [library]
Relations_1_facts [library]
Relations_2_facts [library]
Relations_3_facts [library]
Rel_of_transitive [lemma, in CoursDeCoq.Partial_order_facts]
Rel_of_antisymmetric [lemma, in CoursDeCoq.Partial_order_facts]
Rel_of_reflexive [lemma, in CoursDeCoq.Partial_order_facts]
Rel_of [lemma, in CoursDeCoq.podefs]
resolution [lemma, in CoursDeCoq.ex1]
resolution [lemma, in CoursDeCoq.ex1_auto]
Rplus [inductive, in CoursDeCoq.Relations_2]
Rplus_n [constructor, in CoursDeCoq.Relations_2]
Rplus_0 [constructor, in CoursDeCoq.Relations_2]
Rplus_contains_R [lemma, in CoursDeCoq.Relations_2_facts]
Rstar [inductive, in CoursDeCoq.Relations_2]
RstarRplus_RRstar [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_n [constructor, in CoursDeCoq.Relations_2]
Rstar_0 [constructor, in CoursDeCoq.Relations_2]
Rstar_equiv_Rstar1 [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_cases [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_transitive [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_contains_Rplus [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_contains_R [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_reflexive [lemma, in CoursDeCoq.Relations_2_facts]
Rstar_imp_coherent [lemma, in CoursDeCoq.Relations_3_facts]
Rstar1 [inductive, in CoursDeCoq.Relations_2]
Rstar1_n [constructor, in CoursDeCoq.Relations_2]
Rstar1_1 [constructor, in CoursDeCoq.Relations_2]
Rstar1_0 [constructor, in CoursDeCoq.Relations_2]
Rsym_imp_Rstarsym [lemma, in CoursDeCoq.Relations_2_facts]
Rsym_imp_notRsym [lemma, in CoursDeCoq.Relations_1_facts]

## S

S [lemma, in CoursDeCoq.ex1]
S [lemma, in CoursDeCoq.ex1_auto]
same_relation [definition, in CoursDeCoq.Relations_1]
Same_set_intro [lemma, in CoursDeCoq.Ensembles]
Same_set [definition, in CoursDeCoq.Ensembles]
Same_set_reflexive [lemma, in CoursDeCoq.ps]
Same_set_equivalence [lemma, in CoursDeCoq.ps]
same_relation_is_equivalence [lemma, in CoursDeCoq.Relations_1_facts]
Setminus [inductive, in CoursDeCoq.Ensembles]
Setminus_intro [constructor, in CoursDeCoq.Ensembles]
Simple [lemma, in CoursDeCoq.ex1]
Simple [lemma, in CoursDeCoq.ex1_auto]
Singleton [inductive, in CoursDeCoq.Ensembles]
Singleton_has_lub [lemma, in CoursDeCoq.Partial_order_facts]
Singleton_is_finite [lemma, in CoursDeCoq.ps]
SRel_of [definition, in CoursDeCoq.podefs]
Sstar_contains_Rstar [lemma, in CoursDeCoq.Relations_2_facts]
star_monotone [lemma, in CoursDeCoq.Relations_2_facts]
Strongly_confluent [definition, in CoursDeCoq.Relations_2]
Strong_confluence_direct [lemma, in CoursDeCoq.Relations_3_facts]
Strong_confluence [lemma, in CoursDeCoq.Relations_3_facts]
Symmetric [definition, in CoursDeCoq.Relations_1]

## T

The_power_set_partial_order.A [variable, in CoursDeCoq.ps]
The_power_set_partial_order.U [variable, in CoursDeCoq.ps]
The_power_set_partial_order [section, in CoursDeCoq.ps]
Totally_ordered_definition [constructor, in CoursDeCoq.podefs_1]
Totally_ordered [inductive, in CoursDeCoq.podefs_1]
Transitive [definition, in CoursDeCoq.Relations_1]
trivial [lemma, in CoursDeCoq.ex1]
trivial [lemma, in CoursDeCoq.ex1_auto]

## U

Union [inductive, in CoursDeCoq.Ensembles]
Union_is_finite [constructor, in CoursDeCoq.Ensembles]
Union_intror [constructor, in CoursDeCoq.Ensembles]
Union_introl [constructor, in CoursDeCoq.Ensembles]
Union_of_finite_is_finite [lemma, in CoursDeCoq.ps]
Union_associative [lemma, in CoursDeCoq.ps]
Union_commutative [lemma, in CoursDeCoq.ps]
Union_is_Lub [lemma, in CoursDeCoq.ps]
Union_increases_r [lemma, in CoursDeCoq.ps]
Union_increases_l [lemma, in CoursDeCoq.ps]
Union_minimal [lemma, in CoursDeCoq.ps]
Upper_Bound_definition [constructor, in CoursDeCoq.podefs_1]
Upper_Bound [inductive, in CoursDeCoq.podefs_1]
Upper_downward_stable [lemma, in CoursDeCoq.Partial_order_facts]

## W

Witnesses [lemma, in CoursDeCoq.ex1]
Witnesses [lemma, in CoursDeCoq.ex1_auto]

# Variable Index

## B

Bounds.C [in CoursDeCoq.podefs_1]
Bounds.D [in CoursDeCoq.podefs_1]
Bounds.R [in CoursDeCoq.podefs_1]
Bounds.U [in CoursDeCoq.podefs_1]

## E

Ensembles.U [in CoursDeCoq.Ensembles]

## F

First_inductive_lemmas.D [in CoursDeCoq.Fil]
First_inductive_lemmas.B [in CoursDeCoq.Fil]
First_inductive_lemmas.U [in CoursDeCoq.Fil]

## L

Lemmas_on_partial_orders.D [in CoursDeCoq.Partial_order_facts]
Lemmas_on_partial_orders.B [in CoursDeCoq.Partial_order_facts]
Lemmas_on_partial_orders.U [in CoursDeCoq.Partial_order_facts]

## P

Partial_orders.U [in CoursDeCoq.podefs]

## R

Relations_1.R [in CoursDeCoq.Relations_1]
Relations_1.U [in CoursDeCoq.Relations_1]
Relations_2.R [in CoursDeCoq.Relations_2]
Relations_2.U [in CoursDeCoq.Relations_2]
Relations_3.R [in CoursDeCoq.Relations_3]
Relations_3.U [in CoursDeCoq.Relations_3]

## T

The_power_set_partial_order.A [in CoursDeCoq.ps]
The_power_set_partial_order.U [in CoursDeCoq.ps]

# Library Index

drinker

Ensembles
ex1
ex1_auto

Fil

## P

Partial_order_facts
podefs
podefs_1
ps

## R

Relations_2
Relations_3
Relations_1
Relations_1_facts
Relations_2_facts
Relations_3_facts

# Constructor Index

## B

Bottom_definition [in CoursDeCoq.podefs_1]

## C

Couple_r [in CoursDeCoq.Ensembles]
Couple_l [in CoursDeCoq.Ensembles]

## D

Definition_of_Conditionally_complete [in CoursDeCoq.podefs_1]
Definition_of_Complete [in CoursDeCoq.podefs_1]
Definition_of_Directed [in CoursDeCoq.podefs_1]
Definition_of_PO [in CoursDeCoq.podefs]
Definition_of_PER [in CoursDeCoq.Relations_1]
Definition_of_equivalence [in CoursDeCoq.Relations_1]
Definition_of_order [in CoursDeCoq.Relations_1]
Definition_of_preorder [in CoursDeCoq.Relations_1]
Definition_of_Power_set [in CoursDeCoq.ps]
definition_of_noetherian [in CoursDeCoq.Relations_3]
Disjoint_intro [in CoursDeCoq.Ensembles]

## E

Empty_is_finite [in CoursDeCoq.Ensembles]

## G

Glb_definition [in CoursDeCoq.podefs_1]

## I

Intersection_intro [in CoursDeCoq.Ensembles]
In_singleton [in CoursDeCoq.Ensembles]

## L

Lower_Bound_definition [in CoursDeCoq.podefs_1]
Lub_definition [in CoursDeCoq.podefs_1]

## N

Non_empty_intro [in CoursDeCoq.Ensembles]

## R

Rplus_n [in CoursDeCoq.Relations_2]
Rplus_0 [in CoursDeCoq.Relations_2]
Rstar_n [in CoursDeCoq.Relations_2]
Rstar_0 [in CoursDeCoq.Relations_2]
Rstar1_n [in CoursDeCoq.Relations_2]
Rstar1_1 [in CoursDeCoq.Relations_2]
Rstar1_0 [in CoursDeCoq.Relations_2]

## S

Setminus_intro [in CoursDeCoq.Ensembles]

## T

Totally_ordered_definition [in CoursDeCoq.podefs_1]

## U

Union_is_finite [in CoursDeCoq.Ensembles]
Union_intror [in CoursDeCoq.Ensembles]
Union_introl [in CoursDeCoq.Ensembles]
Upper_Bound_definition [in CoursDeCoq.podefs_1]

# Lemma Index

## A

and_commutative [in CoursDeCoq.ex1]
and_commutative [in CoursDeCoq.ex1_auto]

## C

Carrier_of [in CoursDeCoq.podefs]
coherent_symmetric [in CoursDeCoq.Relations_3_facts]
Compatible_is_symmetric [in CoursDeCoq.Partial_order_facts]
Compatible_is_reflexive [in CoursDeCoq.Partial_order_facts]
Conditionally_complete_has_a_bottom [in CoursDeCoq.Partial_order_facts]
contains_is_preorder [in CoursDeCoq.Relations_1_facts]
Couple_is_symmetric [in CoursDeCoq.Partial_order_facts]
Couple_included_in_carrier [in CoursDeCoq.Partial_order_facts]

## D

drinker's_theorem [in CoursDeCoq.drinker]

## E

Empty_set_has_lub [in CoursDeCoq.Partial_order_facts]
Empty_set_has_Upper_Bound [in CoursDeCoq.Partial_order_facts]
Empty_set_zero [in CoursDeCoq.ps]
Empty_set_is_Bottom [in CoursDeCoq.ps]
Empty_set_minimal [in CoursDeCoq.ps]
Equiv_from_order [in CoursDeCoq.Relations_1_facts]
Equiv_from_preorder [in CoursDeCoq.Relations_1_facts]

## F

Finite_plus_one_is_finite [in CoursDeCoq.ps]

## I

Inclusion_is_transitive [in CoursDeCoq.ps]
Inclusion_is_an_order [in CoursDeCoq.ps]
Intersection_is_Glb [in CoursDeCoq.ps]
Intersection_decreases_r [in CoursDeCoq.ps]
Intersection_decreases_l [in CoursDeCoq.ps]
Intersection_maximal [in CoursDeCoq.ps]

## L

Lemma1 [in CoursDeCoq.Relations_2_facts]
Lub_is_in_Carrier [in CoursDeCoq.Partial_order_facts]

## M

mini_cases [in CoursDeCoq.ex1]
mini_cases [in CoursDeCoq.ex1_auto]
mp [in CoursDeCoq.ex1]
mp [in CoursDeCoq.ex1_auto]

## N

Newman [in CoursDeCoq.Relations_3_facts]
Noetherian_contains_Noetherian [in CoursDeCoq.Relations_3_facts]
Non_disjoint_union [in CoursDeCoq.ps]
not_quite_classic [in CoursDeCoq.ex1]
not_not_converse [in CoursDeCoq.ex1]
not_not [in CoursDeCoq.ex1]
not_quite_classic [in CoursDeCoq.ex1_auto]
not_not_converse [in CoursDeCoq.ex1_auto]
not_not [in CoursDeCoq.ex1_auto]

## O

or_commutative [in CoursDeCoq.ex1]
or_commutative [in CoursDeCoq.ex1_auto]

## P

Pairs_are_enough [in CoursDeCoq.Fil]
Pairs_are_enough_finite_case [in CoursDeCoq.Fil]
Peirce [in CoursDeCoq.ex1_auto]
Power_set_PO [in CoursDeCoq.ps]
Power_set_non_empty [in CoursDeCoq.ps]
Praeclarum [in CoursDeCoq.ex1]
Praeclarum [in CoursDeCoq.ex1_auto]

## R

Rel_of_transitive [in CoursDeCoq.Partial_order_facts]
Rel_of_antisymmetric [in CoursDeCoq.Partial_order_facts]
Rel_of_reflexive [in CoursDeCoq.Partial_order_facts]
Rel_of [in CoursDeCoq.podefs]
resolution [in CoursDeCoq.ex1]
resolution [in CoursDeCoq.ex1_auto]
Rplus_contains_R [in CoursDeCoq.Relations_2_facts]
RstarRplus_RRstar [in CoursDeCoq.Relations_2_facts]
Rstar_equiv_Rstar1 [in CoursDeCoq.Relations_2_facts]
Rstar_cases [in CoursDeCoq.Relations_2_facts]
Rstar_transitive [in CoursDeCoq.Relations_2_facts]
Rstar_contains_Rplus [in CoursDeCoq.Relations_2_facts]
Rstar_contains_R [in CoursDeCoq.Relations_2_facts]
Rstar_reflexive [in CoursDeCoq.Relations_2_facts]
Rstar_imp_coherent [in CoursDeCoq.Relations_3_facts]
Rsym_imp_Rstarsym [in CoursDeCoq.Relations_2_facts]
Rsym_imp_notRsym [in CoursDeCoq.Relations_1_facts]

## S

S [in CoursDeCoq.ex1]
S [in CoursDeCoq.ex1_auto]
Same_set_intro [in CoursDeCoq.Ensembles]
Same_set_reflexive [in CoursDeCoq.ps]
Same_set_equivalence [in CoursDeCoq.ps]
same_relation_is_equivalence [in CoursDeCoq.Relations_1_facts]
Simple [in CoursDeCoq.ex1]
Simple [in CoursDeCoq.ex1_auto]
Singleton_has_lub [in CoursDeCoq.Partial_order_facts]
Singleton_is_finite [in CoursDeCoq.ps]
Sstar_contains_Rstar [in CoursDeCoq.Relations_2_facts]
star_monotone [in CoursDeCoq.Relations_2_facts]
Strong_confluence_direct [in CoursDeCoq.Relations_3_facts]
Strong_confluence [in CoursDeCoq.Relations_3_facts]

## T

trivial [in CoursDeCoq.ex1]
trivial [in CoursDeCoq.ex1_auto]

## U

Union_of_finite_is_finite [in CoursDeCoq.ps]
Union_associative [in CoursDeCoq.ps]
Union_commutative [in CoursDeCoq.ps]
Union_is_Lub [in CoursDeCoq.ps]
Union_increases_r [in CoursDeCoq.ps]
Union_increases_l [in CoursDeCoq.ps]
Union_minimal [in CoursDeCoq.ps]
Upper_downward_stable [in CoursDeCoq.Partial_order_facts]

## W

Witnesses [in CoursDeCoq.ex1]
Witnesses [in CoursDeCoq.ex1_auto]

# Axiom Index

## E

Extensionality_Ensembles [in CoursDeCoq.Ensembles]

# Inductive Index

## B

Bottom [in CoursDeCoq.podefs_1]

## C

Complete [in CoursDeCoq.podefs_1]
Conditionally_complete [in CoursDeCoq.podefs_1]
Couple [in CoursDeCoq.Ensembles]

## D

Directed [in CoursDeCoq.podefs_1]
Disjoint [in CoursDeCoq.Ensembles]

## E

Empty_set [in CoursDeCoq.Ensembles]
Equivalence [in CoursDeCoq.Relations_1]

## F

Finite [in CoursDeCoq.Ensembles]

## G

Glb [in CoursDeCoq.podefs_1]

## I

Intersection [in CoursDeCoq.Ensembles]

## L

Lower_Bound [in CoursDeCoq.podefs_1]
Lub [in CoursDeCoq.podefs_1]

## N

noetherian [in CoursDeCoq.Relations_3]
Non_empty [in CoursDeCoq.Ensembles]

## O

Order [in CoursDeCoq.Relations_1]

## P

PER [in CoursDeCoq.Relations_1]
PO [in CoursDeCoq.podefs]
Power_set [in CoursDeCoq.ps]
Preorder [in CoursDeCoq.Relations_1]

## R

Rplus [in CoursDeCoq.Relations_2]
Rstar [in CoursDeCoq.Relations_2]
Rstar1 [in CoursDeCoq.Relations_2]

## S

Setminus [in CoursDeCoq.Ensembles]
Singleton [in CoursDeCoq.Ensembles]

## T

Totally_ordered [in CoursDeCoq.podefs_1]

## U

Union [in CoursDeCoq.Ensembles]
Upper_Bound [in CoursDeCoq.podefs_1]

# Section Index

## B

Bounds [in CoursDeCoq.podefs_1]

## E

Ensembles [in CoursDeCoq.Ensembles]

## F

First_inductive_lemmas [in CoursDeCoq.Fil]

## L

Lemmas_on_partial_orders [in CoursDeCoq.Partial_order_facts]

## P

Partial_orders [in CoursDeCoq.podefs]

## R

Relations_1 [in CoursDeCoq.Relations_1]
Relations_2 [in CoursDeCoq.Relations_2]
Relations_3 [in CoursDeCoq.Relations_3]

## T

The_power_set_partial_order [in CoursDeCoq.ps]

# Definition Index

## A

Antisymmetric [in CoursDeCoq.Relations_1]

## C

Carrier [in CoursDeCoq.podefs]
Chain [in CoursDeCoq.podefs_1]
coherent [in CoursDeCoq.Relations_3]
Compatible [in CoursDeCoq.podefs_1]
Complement [in CoursDeCoq.Relations_1_facts]
Confluent [in CoursDeCoq.Relations_3]
confluent [in CoursDeCoq.Relations_3]
contains [in CoursDeCoq.Relations_1]
Cpo [in CoursDeCoq.podefs_1]

## E

Ensemble [in CoursDeCoq.Ensembles]

## I

In [in CoursDeCoq.Ensembles]
Included [in CoursDeCoq.Ensembles]

## L

Locally_confluent [in CoursDeCoq.Relations_3]
locally_confluent [in CoursDeCoq.Relations_3]

## N

Noetherian [in CoursDeCoq.Relations_3]

## R

Reflexive [in CoursDeCoq.Relations_1]
Rel [in CoursDeCoq.podefs]
Relation [in CoursDeCoq.Relations_1]

## S

same_relation [in CoursDeCoq.Relations_1]
Same_set [in CoursDeCoq.Ensembles]
SRel_of [in CoursDeCoq.podefs]
Strongly_confluent [in CoursDeCoq.Relations_2]
Symmetric [in CoursDeCoq.Relations_1]

## T

Transitive [in CoursDeCoq.Relations_1]

 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 (224 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 (20 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 (15 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 (34 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 (92 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 (1 entry) 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 (28 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 (9 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 (25 entries)