Library Coq.Relations.Operators_Properties
Some properties of the operators on relations
Initial version by Bruno Barras
Correctness of the reflexive-transitive closure operator
Idempotency of the reflexive-transitive closure operator
Reflexive-transitive closure is included in the
reflexive-symmetric-transitive closure
Correctness of the reflexive-symmetric-transitive closure
Idempotency of the reflexive-symmetric-transitive closure operator
Equivalences between the different definition of the reflexive,
symmetric, transitive closures
Contributed by P. Castéran
Direct transitive closure vs left-step extension
Direct transitive closure vs right-step extension
Direct reflexive-transitive closure is equivalent to
transitivity by left-step extension
Direct reflexive-transitive closure is equivalent to
transitivity by right-step extension
Induction on the left transitive step
Induction on the right transitive step
Direct reflexive-symmetric-transitive closure is equivalent to
transitivity by symmetric left-step extension
Direct reflexive-symmetric-transitive closure is equivalent to
transitivity by symmetric right-step extension