Library Coq.Relations.Relation_Operators
Bruno Barras, Cristina Cornes
Some of these definitions were taken from :
Constructing Recursion Operators in Type Theory
L. Paulson JSC (1986) 2, 325-355
Some operators to build relations
Definition by direct transitive closure
Alternative definition by transitive extension on the left
Alternative definition by transitive extension on the right
Reflexive-transitive closure
Definition by direct reflexive-transitive closure
Alternative definition by transitive extension on the left
Alternative definition by transitive extension on the right
Reflexive-symmetric-transitive closure
Definition by direct reflexive-symmetric-transitive closure
Alternative definition by symmetric-transitive extension on the left
Alternative definition by symmetric-transitive extension on the right
Disjoint union of relations
Lexicographic order on dependent pairs
Multiset of two relations