# Library Coq.Sets.Relations_1_facts

Require Export Relations_1.

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).
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).
Hint Resolve Equiv_from_order : core.

Theorem contains_is_preorder :
forall U:Type, Preorder (Relation U) (contains U).
Hint Resolve contains_is_preorder : core.

Theorem same_relation_is_equivalence :
forall U:Type, Equivalence (Relation U) (same_relation U).
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'.