The Coq Proof Assistant

# Library Coq.Sets.Relations_1_facts

Require Export Relations_1.
Local Ltac Tauto.intuition_solver ::= auto with sets.
Definition Complement (U:Type) (R:Relation U) : Relation U :=
fun x y:U => ~ R x y.
Theorem Rsym_imp_notRsym :
forall (U:Type) (R:Relation U),
Symmetric U R -> Symmetric U (Complement U R).
Theorem Equiv_from_preorder :
forall (U:Type) (R:Relation U),
Preorder U R -> Equivalence U (fun x y:U => R x y /\ R y x).
#[global]
Hint Resolve Equiv_from_preorder : core.
Theorem Equiv_from_order :
forall (U:Type) (R:Relation U),
Order U R -> Equivalence U (fun x y:U => R x y /\ R y x).
#[global]
Hint Resolve Equiv_from_order : core.
Theorem contains_is_preorder :
forall U:Type, Preorder (Relation U) (contains U).
#[global]
Hint Resolve contains_is_preorder : core.
Theorem same_relation_is_equivalence :
forall U:Type, Equivalence (Relation U) (same_relation U).
#[global]
Hint Resolve same_relation_is_equivalence : core.
Theorem cong_reflexive_same_relation :
forall (U:Type) (R R':Relation U),
same_relation U R R' -> Reflexive U R -> Reflexive U R'.
Theorem cong_symmetric_same_relation :
forall (U:Type) (R R':Relation U),
same_relation U R R' -> Symmetric U R -> Symmetric U R'.
Theorem cong_antisymmetric_same_relation :
forall (U:Type) (R R':Relation U),
same_relation U R R' -> Antisymmetric U R -> Antisymmetric U R'.
Theorem cong_transitive_same_relation :
forall (U:Type) (R R':Relation U),
same_relation U R R' -> Transitive U R -> Transitive U R'.