Library Subsets.Binary_relation

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Support for homogeneous binary relations on any type.

Description

In the sequel, "homogeneous binary relation" is often simplify into "binary relation". Interesting binary relations are transitive.
Let T be any type. Let R R1 R2 : T T Prop be homogeneous binary relations on T.

Operators

Elementary properties

  • reflexive R means that each element is related to itself (through R).
  • irreflexive R means that no element is related to itself.
  • symmetric R means that any relation R x y implies its converse R y x.
  • antisymmetric R means that if any relation R x y and its converse R y x both hold, then the arguments are equal, x = y.
  • connected R means that all distincts elements are comparable, ie for all x y, either relation R x y or its converse R y x holds.
  • asymmetric R means that when a relation R x y holds, then its converse R y x never holds.
  • strongly_connected R means that all elements are comparable, ie for all x y, either relation R x y, or its converse R y x holds.
  • trichotomous R means that we have either x = y, R x y, or R y x (meaning exclusive or).
  • transitive R means that if relations R x y and R y z hold, then relation R x z also holds.
  • negatively_transitive R means that if relations ¬ R x y and ¬ R y z hold, then relation ¬ R x z also holds, ie complement R is transitive.

Compound properties

  • partial_equivalence_relation R means that R is transitive and symmetric.
  • equivalence_relation R means that R is transitive, reflexive and symmetric, ie R is a reflexive partial equivalence relation.
  • preorder R means that R is transitive and reflexive.
  • total_preorder R means that R is transitive, reflexive and strongly connected, ie R is a strongly connected preorder.
  • partial_order R means that R is transitive, reflexive and antisymmetric.
  • total_order R means that R is transitive, reflexive, antisymmetric and strongly connected, ie R is a strongly connected partial order.
  • strict_partial_order R means that R is transitive, irreflexive and asymmetric.
  • strict_total_order R means that R is transitive, irreflexive, asymmetric and connected, ie R is a connected strict partial order.
  • strict_weak_order R means that R is negatively transitive, irreflexive and asymmetric.

Bibliography

[Ehrgott] Matthias Ehrgott, Multicriteria Optimization, 2nd edition, Springer, 2005.
[HR] https://en.wikipedia.org/wiki/Homogeneous_relation.

Used logic axioms

  • classic, the weak form of excluded middle;
  • decidability of equality in type T is explicitely assumed for some results.

Usage

This module may be used through the import of Subsets.Subsets, Subsets.Subsets_wDep, Algebra.Algebra_wDep, Lebesgue.Lebesgue_p_wDep, or Lebesgue.Bochner.Bochner_wDep, where it is exported.

From Requisite Require Import stdlib ssr_wMC.

From Logic Require Import logic_compl.
From Subsets Require Import Subset Function.

Section Homogeneous_binary_relation_Def1.

Operators on homogeneous binary relations.

Context {T : Type}.
Variable R R1 R2 : T T Prop.

Definition converse : T T Prop := fun x yR y x.
Definition complementary : T T Prop := fun x y¬ R x y.
Definition conv_compl : T T Prop := fun x y¬ R y x.

Definition br_empty : T T Prop := fun _ _False.
Definition br_universal : T T Prop := fun _ _True.

Definition br_and : T T Prop := fun x yR1 x y R2 x y.
Definition br_or : T T Prop := fun x yR1 x y R2 x y.

Definition br_and_neq : T T Prop := fun x yx y R x y.
Definition br_or_eq : T T Prop := fun x yx = y R x y.

Definition strict : T T Prop := fun x yR x y ¬ R y x.
Definition equivalent : T T Prop := fun x yR x y R y x.

Definition comparable : T T Prop := fun x yR x y R y x.
Definition incomparable : T T Prop := fun x y¬ R x y ¬ R y x.

End Homogeneous_binary_relation_Def1.

Section Homogeneous_binary_relation_Def2.

Elementary properties of homogeneous binary relations.

Context {T : Type}.
Variable R : T T Prop.

Definition reflexive : Prop := x, R x x.
Definition irreflexive : Prop := x, ¬ R x x.

Definition symmetric : Prop := x y, R x y R y x.

Definition antisymmetric : Prop := x y, R x y R y x x = y.
Definition connected : Prop := x y, x y R x y R y x.

Definition asymmetric : Prop := x y, R x y ¬ R y x.
Definition strongly_connected : Prop := x y, R x y R y x.

Definition trichotomous : Prop :=
   x y, x = y ¬ R x y ¬ R y x
    x y R x y ¬ R y x x y R y x ¬ R x y.

Definition transitive : Prop := x y z, R x y R y z R x z.
Definition negatively_transitive : Prop :=
   x y z, ¬ R x y ¬ R y z ¬ R x z.

End Homogeneous_binary_relation_Def2.

Section Homogeneous_binary_relation_Def3.

Compound properties of homogeneous binary relations.
Results about operators on homogeneous binary relations.

Context {T : Type}.

About the converse / complementary / conv_compl (unary) operators.

Lemma conv_inj : injective (@converse T).
Proof. move=>> /fun_ext2_rev H; apply fun_ext2; intros; apply H. Qed.

Lemma conv_invol : involutive (@converse T).
Proof. easy. Qed.

Lemma conv_eq : converse eq = @eq T.
Proof. apply fun_ext2; intros; apply prop_ext; split; apply eq_sym. Qed.

Lemma conv_neq : converse neq = @neq T.
Proof. apply fun_ext2; intros; apply prop_ext; split; apply not_eq_sym. Qed.

Lemma conv_fix_equiv : {R : T T Prop}, converse R = R symmetric R.
Proof.
intros R; split; intros H.
intros x y; rewrite -{2}H; easy.
apply fun_ext2; intros x y; apply prop_ext; split; apply H.
Qed.

Lemma compl_alt :
   {R : T T Prop} x y, complementary R x y ¬ R x y.
Proof. easy. Qed.

Lemma compl_inj : injective (@complementary T).
Proof.
move=>> /fun_ext2_rev H; apply fun_ext2; intros; apply prop_ext, iff_not_equiv.
unfold complementary in H; rewrite (H x1 x2); easy.
Qed.

Lemma br_compl_invol : involutive (@complementary T).
Proof. intros R; apply fun_ext; intros x; apply compl_invol. Qed.

Lemma compl_eq : complementary (@eq T) = neq.
Proof. easy. Qed.

Lemma compl_neq : complementary (@neq T) = eq.
Proof. rewrite -compl_eq; apply br_compl_invol. Qed.

Lemma conv_compl_alt :
   {R : T T Prop} x y, conv_compl R x y ¬ R y x.
Proof. easy. Qed.

Lemma compl_conv_eq :
   {R : T T Prop},
    complementary (converse R) = converse (complementary R).
Proof. easy. Qed.

Lemma conv_compl_eq_comp : @conv_compl T = converse \o complementary.
Proof. easy. Qed.

Lemma conv_compl_eq :
   {R : T T Prop}, conv_compl R = converse (complementary R).
Proof. easy. Qed.

Lemma conv_compl_eq_alt :
   {R : T T Prop}, conv_compl R = complementary (converse R).
Proof. easy. Qed.

Lemma conv_compl_inj : injective (@conv_compl T).
Proof. apply (inj_comp conv_inj compl_inj). Qed.

Lemma conv_conv_compl :
   {R : T T Prop}, converse (conv_compl R) = complementary R.
Proof. intros; rewrite conv_compl_eq conv_invol; easy. Qed.

Lemma compl_conv_compl :
   {R : T T Prop}, complementary (conv_compl R) = converse R.
Proof. intros; rewrite conv_compl_eq_alt br_compl_invol; easy. Qed.

Lemma conv_compl_invol : involutive (@conv_compl T).
Proof.
rewrite conv_compl_eq_comp; apply invol_comp;
    [| apply conv_invol | apply br_compl_invol].
apply fun_ext; intros; apply eq_sym, compl_conv_eq.
Qed.

About the br_empty / br_universal (0-ary) operators.

Lemma neq_br_empty_equiv :
   {R : T T Prop}, R br_empty x y, R x y.
Proof.
intros; rewrite iff_not_l_equiv not_ex_all_not_equiv; split.
intros; subst; intros [y Hy]; easy.
intros H; apply fun_ext2; intros x y; apply prop_ext; split; [| easy].
intros H1; apply (H x); y; easy.
Qed.

About the br_and / br_or (binary) operators.

Lemma br_and_conv :
   {R1 R2 : T T Prop},
    br_and (converse R1) (converse R2) = converse (br_and R1 R2).
Proof. easy. Qed.

Lemma br_or_conv :
   {R1 R2 : T T Prop},
    br_or (converse R1) (converse R2) = converse (br_or R1 R2).
Proof. easy. Qed.

Lemma br_and_compl :
   {R1 R2 : T T Prop},
    br_and (complementary R1) (complementary R2) = complementary (br_or R1 R2).
Proof.
intros; apply fun_ext2; intros; apply prop_ext, iff_sym, not_or_equiv.
Qed.

Lemma br_or_compl :
   {R1 R2 : T T Prop},
    br_or (complementary R1) (complementary R2) = complementary (br_and R1 R2).
Proof.
intros; apply fun_ext2; intros; apply prop_ext, iff_sym, not_and_equiv.
Qed.

Lemma br_and_conv_compl :
   {R1 R2 : T T Prop},
    br_and (conv_compl R1) (conv_compl R2) = conv_compl (br_or R1 R2).
Proof. intros; rewrite br_and_conv br_and_compl; easy. Qed.

Lemma br_or_conv_compl :
   {R1 R2 : T T Prop},
    br_or (conv_compl R1) (conv_compl R2) = conv_compl (br_and R1 R2).
Proof. intros; rewrite br_or_conv br_or_compl; easy. Qed.

About the br_and_neq / br_or_eq (unary) operators.

Lemma br_and_neq_eq :
   {R : T T Prop}, br_and_neq R = br_and (@neq T) R.
Proof. easy. Qed.

Lemma br_or_eq_eq : {R : T T Prop}, br_or_eq R = br_or (@eq T) R.
Proof. easy. Qed.

Lemma br_and_neq_eq_strict :
   {R : T T Prop}, antisymmetric R br_and_neq R = strict R.
Proof.
intros R H; apply fun_ext2; intros; apply prop_ext; split;
    intros [H1 H2]; split;
    [| contradict H1; apply H | contradict H2; subst |]; easy.
Qed.

Lemma br_and_neq_eq_strict_rev :
   {R : T T Prop}, br_and_neq R = strict R antisymmetric R.
Proof.
intros R H x y H1; rewrite contra_equiv; intros H2.
assert (H3 : strict R x y) by now rewrite -H. apply H3.
Qed.

Lemma br_and_neq_eq_strict_equiv :
   {R : T T Prop}, br_and_neq R = strict R antisymmetric R.
Proof.
intros; split; [apply br_and_neq_eq_strict_rev | apply br_and_neq_eq_strict].
Qed.

Lemma br_and_neq_conv :
   {R : T T Prop},
    br_and_neq (converse R) = converse (br_and_neq R).
Proof. intros; rewrite br_and_neq_eq -br_and_conv conv_neq; easy. Qed.

Lemma br_or_eq_conv :
   {R : T T Prop},
    br_or_eq (converse R) = converse (br_or_eq R).
Proof. intros; rewrite br_or_eq_eq -br_or_conv conv_eq; easy. Qed.

Lemma br_and_neq_compl :
   {R : T T Prop},
    br_and_neq (complementary R) = complementary (br_or_eq R).
Proof. intros; rewrite br_and_neq_eq -br_and_compl compl_eq; easy. Qed.

Lemma br_or_eq_compl :
   {R : T T Prop},
    br_or_eq (complementary R) = complementary (br_and_neq R).
Proof. intros; rewrite br_or_eq_eq -br_or_compl compl_neq; easy. Qed.

Lemma br_and_neq_conv_compl :
   {R : T T Prop},
    br_and_neq (conv_compl R) = conv_compl (br_or_eq R).
Proof. intros; rewrite br_and_neq_conv br_and_neq_compl; easy. Qed.

Lemma br_or_eq_conv_compl :
   {R : T T Prop},
    br_or_eq (conv_compl R) = conv_compl (br_and_neq R).
Proof. intros; rewrite br_or_eq_conv br_or_eq_compl; easy. Qed.

About the strict / equivalent (unary) operators.

Lemma strict_eq :
   {R : T T Prop}, strict R = br_and R (conv_compl R).
Proof. easy. Qed.

Lemma strict_conv_eq_compl :
   {R : T T Prop}, strict (converse R) = strict (complementary R).
Proof.
intros; apply fun_ext2; intros; apply prop_ext;
    unfold strict; rewrite NNPP_equiv; apply and_comm.
Qed.

Lemma strict_compl_eq_conv :
   {R : T T Prop}, strict (complementary R) = strict (converse R).
Proof. intros; apply eq_sym, strict_conv_eq_compl. Qed.

Lemma strict_conv_compl :
   {R : T T Prop}, strict (conv_compl R) = strict R.
Proof. intros; rewrite strict_conv_eq_compl br_compl_invol; easy. Qed.

Lemma conv_strict :
   {R : T T Prop}, converse (strict R) = strict (converse R).
Proof. easy. Qed.

Lemma compl_strict :
   {R : T T Prop},
    complementary (strict R) = br_or (complementary R) (converse R).
Proof. intros; rewrite strict_eq -br_or_compl compl_conv_compl; easy. Qed.

Lemma equivalent_eq :
   {R : T T Prop}, equivalent R = br_and R (converse R).
Proof. easy. Qed.

About the comparable / incomparable (unary) operators.

Lemma compar_eq :
   {R : T T Prop}, comparable R = br_or R (converse R).
Proof. easy. Qed.

Lemma incompar_eq :
   {R : T T Prop},
    incomparable R = br_and (complementary R) (conv_compl R).
Proof. easy. Qed.

Lemma incompar_eq_alt :
   {R : T T Prop}, incomparable R = equivalent (complementary R).
Proof. easy. Qed.

Lemma compar_idem :
   {R : T T Prop}, comparable (comparable R) = comparable R.
Proof.
unfold comparable; intros; apply fun_ext2; intros; apply prop_ext; tauto.
Qed.

Lemma incomp2 :
   {R : T T Prop}, incomparable (incomparable R) = comparable R.
Proof.
unfold incomparable, comparable;
    intros; apply fun_ext2; intros; apply prop_ext; tauto.
Qed.

Lemma compar_incompar :
   {R : T T Prop}, comparable (incomparable R) = incomparable R.
Proof.
unfold incomparable, comparable;
    intros; apply fun_ext2; intros; apply prop_ext; tauto.
Qed.

Lemma incompar_compar :
   {R : T T Prop}, incomparable (comparable R) = incomparable R.
Proof.
unfold incomparable, comparable;
    intros; apply fun_ext2; intros; apply prop_ext; tauto.
Qed.

Lemma conv_compar :
   {R : T T Prop}, converse (comparable R) = comparable R.
Proof. intros; apply fun_ext2; intros; apply prop_ext, or_comm. Qed.

Lemma compar_conv :
   {R : T T Prop}, comparable (converse R) = comparable R.
Proof. intros; apply fun_ext2; intros; apply prop_ext, or_comm. Qed.

Lemma conv_incompar :
   {R : T T Prop}, converse (incomparable R) = incomparable R.
Proof. intros; apply fun_ext2; intros; apply prop_ext, and_comm. Qed.

Lemma incompar_conv :
   {R : T T Prop}, incomparable (converse R) = incomparable R.
Proof. intros; apply fun_ext2; intros; apply prop_ext, and_comm. Qed.

Lemma compl_compar :
   {R : T T Prop}, complementary (comparable R) = incomparable R.
Proof. intros; apply eq_sym, br_and_compl. Qed.

Lemma compl_incompar :
   {R : T T Prop}, complementary (incomparable R) = comparable R.
Proof. intros; rewrite -br_or_compl !br_compl_invol; easy. Qed.

Lemma compar_compl :
   {R : T T Prop},
    comparable (complementary R) =
      complementary (incomparable (complementary R)).
Proof. intros; apply compl_inj; rewrite br_compl_invol; apply compl_compar. Qed.

Lemma incompar_compl :
   {R : T T Prop},
    incomparable (complementary R) =
      complementary (comparable (complementary R)).
Proof. intros; apply compl_inj; rewrite br_compl_invol; apply compl_incompar. Qed.

End Homogeneous_binary_relation_Facts1.

Section Homogeneous_binary_relation_Facts2.

Results about elementary properties of homogeneous binary relations.

Context {T : Type}.

Equivalent formulations of elementary properties.

Lemma sym_equiv :
   {R : T T Prop},
    symmetric R ( x y, R x y R y x).
Proof. intros; split; intros H x y; [split; apply H | rewrite H; easy]. Qed.

Lemma antisym_equiv :
   {R : T T Prop},
    antisymmetric R x y, equivalent R x y x = y.
Proof.
intros; split; intros H x y; [intros [H1 H2] | intros H1 H2]; apply H; easy.
Qed.

Lemma asym_equiv :
   {R : T T Prop},
    asymmetric R x y, ¬ (equivalent R x y).
Proof.
intros; split; intros H x y;
    [intros [H1 H2] | intros H1 H2]; apply (H x y); easy.
Qed.

Lemma conn_equiv :
   {R : T T Prop},
    connected R x y, x y comparable R x y.
Proof. easy. Qed.

Lemma str_conn_equiv :
   {R : T T Prop},
    strongly_connected R x y, comparable R x y.
Proof. easy. Qed.

Lemma tricho_equiv :
   {R : T T Prop},
    trichotomous R x y,
    x = y incomparable R x y x y comparable (strict R) x y.
Proof.
intros; split; intros H x y.
destruct (H x y) as [H1 | [H1 | H1]];
    [left; split | right; split; [| left] | right; split; [| right]]; easy.
destruct (H x y) as [H1 | [H1 [H2 | H2]]];
    [left | right; left | right; right]; easy.
Qed.

About the reflexive / irreflexive elementary properties.

Lemma refl_not_irrefl :
   {R : T T Prop}, inhabited T reflexive R ¬ irreflexive R.
Proof. intros R [x] H1 H2; apply (H2 x); easy. Qed.

Lemma irrefl_not_refl :
   {R : T T Prop}, inhabited T irreflexive R ¬ reflexive R.
Proof. intros R [x] H1 H2; apply (H1 x); easy. Qed.

About the symmetric / antisymmetric / asymmetric elementary properties.

Lemma sym_not_antisym :
   {R : T T Prop} (x y : T),
    x y R x y symmetric R ¬ antisymmetric R.
Proof. intros R x y H1 H2 H3 H4; apply H1, H4; [| apply H3]; easy. Qed.

Lemma antisym_not_sym :
   {R : T T Prop} (x y : T),
    x y R x y antisymmetric R ¬ symmetric R.
Proof. intros R x y H1 H2 H3 H4; apply H1, H3; [| apply H4]; easy. Qed.

Lemma antisym_equiv_conn :
   {R : T T Prop}, antisymmetric R connected (complementary R).
Proof.
intros; rewrite antisym_equiv; split; intros H x y; rewrite contra_equiv;
    [rewrite not_or_equiv !NNPP_equiv | rewrite not_and_equiv]; apply H.
Qed.

Lemma sym_not_asym :
   {R : T T Prop}, R br_empty symmetric R ¬ asymmetric R.
Proof.
intro; rewrite neq_br_empty_equiv;
    intros [x [y H]] H1 H2; apply (H2 x y); [| apply H1]; easy.
Qed.

Lemma asym_not_sym :
   {R : T T Prop}, R br_empty asymmetric R ¬ symmetric R.
Proof.
intro; rewrite neq_br_empty_equiv;
    intros [x [y H]] H1 H2; apply (H1 x y); [| apply H2]; easy.
Qed.

Lemma asym_antisym :
   {R : T T Prop}, asymmetric R antisymmetric R.
Proof. intros R H x y H1 H2; exfalso; apply (H _ _ H1 H2). Qed.

Lemma asym_irrefl : {R : T T Prop}, asymmetric R irreflexive R.
Proof. intros R H x H1; apply (H x x); easy. Qed.

Lemma refl_not_asym :
   {R : T T Prop}, inhabited T reflexive R ¬ asymmetric R.
Proof.
intros R H; rewrite contra_not_r_equiv.
move⇒ /asym_irrefl; apply irrefl_not_refl; easy.
Qed.

"w" stands for "with".
Lemma irrefl_asym_w_antisym :
   {R : T T Prop},
    antisymmetric R irreflexive R asymmetric R.
Proof.
moveR H H' x y H1 H2; move: (H _ _ H1 H2) ⇒ H3; subst; apply (H' y), H1.
Qed.

Lemma asym_equiv_irrefl_antisym :
   {R : T T Prop},
    asymmetric R irreflexive R antisymmetric R.
Proof.
intros; split; intros; [split |]; [apply asym_irrefl | apply asym_antisym |
    apply irrefl_asym_w_antisym]; easy.
Qed.

"w" stands for "with".
Lemma irrefl_asym_w_trans :
   {R : T T Prop}, transitive R irreflexive R asymmetric R.
Proof. intros R H H' x y H1 H2; apply (H' x), (H x y x); easy. Qed.

Lemma irrefl_asym_equiv :
   {R : T T Prop}, transitive R irreflexive R asymmetric R.
Proof.
intros; split; [apply irrefl_asym_w_trans; easy | apply asym_irrefl].
Qed.

About the connected / strongly_connected / trichotomous elementary properties.

Lemma conn_equiv_contra :
   {R : T T Prop},
    connected R x y : T, ¬ R x y ¬ R y x x = y.
Proof. intro; split; intros H x y; move: (H x y); tauto. Qed.

Lemma conn_equiv_alt :
   {R : T T Prop},
    eq_dec T connected R x y, R x y x = y R y x.
Proof.
intros R HT; split; intros H x y.
destruct (HT x y) as [H1 | H1]; [right; left; easy |].
destruct (H _ _ H1) as [H2 | H2]; [left | right; right]; easy.
intros H1; destruct (H x y) as [H2 | [H2 | H2]]; [left | | right]; easy.
Qed.

Lemma conn_equiv_dicho :
   {R : T T Prop},
    eq_dec T connected R
     x y, x = y x y comparable R x y.
Proof.
intros R HT; rewrite (conn_equiv_alt HT); split; intros H x y.
destruct (H x y) as [H1 | [H1 | H1]];
    (destruct (HT x y) as [H2 | H2]; [left; easy | right]);
    [split; [| left] | | split; [| right]]; easy.
destruct (H x y) as [H1 | [H1 [H2 | H2]]];
    [right; left | left | right; right]; easy.
Qed.

Lemma conn_equiv_antisym :
   {R : T T Prop}, connected R antisymmetric (complementary R).
Proof. intros; rewrite antisym_equiv_conn br_compl_invol; easy. Qed.

Lemma str_conn_conn :
   {R : T T Prop}, strongly_connected R connected R.
Proof. easy. Qed.

Lemma str_conn_refl :
   {R : T T Prop}, strongly_connected R reflexive R.
Proof. intros R H x; destruct (H x x); easy. Qed.

Lemma conn_str_conn :
   {R : T T Prop},
    eq_dec T reflexive R connected R strongly_connected R.
Proof.
intros R HT H1 H2 x y; destruct (HT x y) as [H | H]; [subst; left; easy |].
destruct (H2 _ _ H); [left | right]; easy.
Qed.

Lemma str_conn_equiv_refl_conn :
   {R : T T Prop},
    eq_dec T strongly_connected R reflexive R connected R.
Proof.
intros; split; intros; [split |]; [apply str_conn_refl | apply str_conn_conn |
    apply conn_str_conn]; easy.
Qed.

Lemma tricho_equiv_asym_conn :
   {R : T T Prop},
    eq_dec T trichotomous R asymmetric R connected R.
Proof.
intros R HT; rewrite tricho_equiv; split; intros H.
split; intros x y H1; destruct (HT x y) as [H2 | H2].
destruct (H x y) as [[_ [_ H3]] | [H3 _]]; easy.
destruct (H x y) as [[H3 _] | [_ [[_ H3] | [_ H3]]]]; easy.
easy.
destruct (H x y) as [[H3 _] | [_ [[H3 _] | [H3 _]]]]; [| left | right]; easy.
intros x y; destruct (HT x y) as [H1 | H1]; [left | right]; split; try easy.
subst; split; apply asym_irrefl; easy.
destruct H as [H2 H3], (H3 _ _ H1) as [H4 | H4]; [left | right]; split;
    try easy; apply (H2 _ _ H4).
Qed.

About the transitive / negative_transitive elementary properties.

Lemma neg_trans_equiv :
   {R : T T Prop},
    negatively_transitive R transitive (complementary R).
Proof. easy. Qed.

Lemma trans_equiv :
   {R : T T Prop},
    transitive R negatively_transitive (complementary R).
Proof. intros; rewrite neg_trans_equiv br_compl_invol; easy. Qed.

Lemma trans_neg_trans :
   {R : T T Prop},
    eq_dec T connected R transitive R negatively_transitive R.
Proof.
intros R HT H1 H2 x y z H3 H4; contradict H3.
destruct (HT y z) as [H5 | H5]; [subst; easy |].
destruct (H1 _ _ H5) as [H6 | H6]; [| apply H2 with z]; easy.
Qed.

Lemma neg_trans_trans :
   {R : T T Prop},
    eq_dec T antisymmetric R negatively_transitive R transitive R.
Proof.
intros R HT; rewrite neg_trans_equiv -{3}(br_compl_invol R)
    antisym_equiv_conn -neg_trans_equiv; apply (trans_neg_trans HT).
Qed.

End Homogeneous_binary_relation_Facts2.

Section Homogeneous_binary_relation_Facts3.

Results about compound properties of homogeneous binary relations.

Context {T : Type}.

About the partial_equivalence_relation / equivalence_relation compound properties.

Lemma equiv_rel_equiv_per :
   {R : T T Prop},
    equivalence_relation R partial_equivalence_relation R reflexive R.
Proof. intro; split; intros [H1 H2]; easy. Qed.

Lemma equiv_rel_equiv_pro :
   {R : T T Prop},
    equivalence_relation R preorder R symmetric R.
Proof. intro; split; intros [H1 H2]; [| repeat split; try apply H1]; easy. Qed.

Lemma equiv_rel_partial_equiv_rel :
   {R : T T Prop},
    equivalence_relation R partial_equivalence_relation R.
Proof. intro; rewrite equiv_rel_equiv_per; easy. Qed.

About the preorder / total_preorder compound properties.

Lemma total_preorder_equiv :
   {R : T T Prop},
    eq_dec T total_preorder R reflexive R transitive R connected R.
Proof.
intros; split; intros H.
repeat split; [..| apply str_conn_conn]; apply H.
repeat split; [..| apply conn_str_conn]; easy.
Qed.

Lemma total_preorder_equiv_pro :
   {R : T T Prop},
    eq_dec T total_preorder R preorder R connected R.
Proof. intros R HT; rewrite (total_preorder_equiv HT) and_assoc; easy. Qed.

Lemma total_preorder_preorder :
   {R : T T Prop}, eq_dec T total_preorder R preorder R.
Proof. intros R HT; rewrite total_preorder_equiv_pro; easy. Qed.

About the partial_order / total_order compound properties.

Lemma partial_order_equiv :
   {R : T T Prop},
    partial_order R preorder R antisymmetric R.
Proof. intro; split; intros [H1 H2]; [| repeat split; try apply H1]; easy. Qed.

Lemma partial_order_preorder :
   {R : T T Prop}, partial_order R preorder R.
Proof. intro; rewrite partial_order_equiv; easy. Qed.

Lemma total_order_equiv_tpro :
   {R : T T Prop},
    total_order R total_preorder R antisymmetric R.
Proof. intro; split; intros [H1 H2]; [| repeat split; try apply H1]; easy. Qed.

Lemma total_order_equiv :
   {R : T T Prop},
    eq_dec T total_order R
    reflexive R antisymmetric R transitive R connected R.
Proof.
intros; split; intros H.
repeat split; [..| apply str_conn_conn]; apply H.
repeat split; [..| apply conn_str_conn]; easy.
Qed.

Lemma total_order_equiv_pro :
   {R : T T Prop},
    eq_dec T total_order R preorder R antisymmetric R connected R.
Proof. intros; rewrite total_order_equiv; unfold preorder; tauto. Qed.

Lemma total_order_equiv_po :
   {R : T T Prop},
    eq_dec T total_order R partial_order R connected R.
Proof. intros; rewrite total_order_equiv; unfold partial_order; tauto. Qed.

Lemma total_order_partial_order :
   {R : T T Prop}, eq_dec T total_order R partial_order R.
Proof. intros R HT; rewrite total_order_equiv_po; easy. Qed.

Lemma total_order_total_preorder :
   {R : T T Prop}, total_order R total_preorder R.
Proof. intro; rewrite total_order_equiv_tpro; easy. Qed.

Lemma total_order_preorder :
   {R : T T Prop}, eq_dec T total_order R preorder R.
Proof. intros R HT; rewrite total_order_equiv_pro; easy. Qed.

About the strict_partial_order / strict_total_order / strict_weak_order compound properties.

Lemma strict_partial_order_equiv_no_asym :
   {R : T T Prop},
    strict_partial_order R irreflexive R transitive R.
Proof.
intro; split; intros [H1 H2];
    [| repeat split; try apply irrefl_asym_w_trans]; easy.
Qed.

Lemma strict_partial_order_equiv_no_irrefl :
   {R : T T Prop},
    strict_partial_order R asymmetric R transitive R.
Proof.
intro; split; intros [H1 H2]; [| split; try apply asym_irrefl]; easy.
Qed.

Lemma strict_total_order_equiv_spo :
   {R : T T Prop},
    strict_total_order R strict_partial_order R connected R.
Proof. intro; split; intros [H1 H2]; [| repeat split; try apply H1]; easy. Qed.

Lemma strict_total_order_equiv_no_asym :
   {R : T T Prop},
    strict_total_order R irreflexive R transitive R connected R.
Proof.
intro; split; intros [H1 H2]; repeat split;
    try apply H1; try apply irrefl_asym_w_trans; easy.
Qed.

Lemma strict_total_order_equiv_no_irrefl :
   {R : T T Prop},
    strict_total_order R asymmetric R transitive R connected R.
Proof.
intro; split; intros [H1 H2]; repeat split;
    try apply H1; try apply asym_irrefl; easy.
Qed.

Lemma strict_total_order_equiv_tricho :
   {R : T T Prop},
    eq_dec T strict_total_order R transitive R trichotomous R.
Proof.
intros; rewrite strict_total_order_equiv_no_irrefl
    tricho_equiv_asym_conn; tauto.
Qed.

Lemma strict_total_order_strict_partial_order :
   {R : T T Prop}, strict_total_order R strict_partial_order R.
Proof. intro; rewrite strict_total_order_equiv_spo; easy. Qed.

Lemma strict_weak_order_equiv :
   {R : T T Prop},
    strict_weak_order R asymmetric R negatively_transitive R.
Proof.
intro; split; intros [H1 H2]; [| split; try apply asym_irrefl]; easy.
Qed.

Lemma strict_total_order_equiv_swo :
   {R : T T Prop},
    eq_dec T strict_total_order R strict_weak_order R connected R.
Proof.
intros R HT; rewrite strict_total_order_equiv_no_irrefl
    strict_weak_order_equiv; split; intros H; repeat split; try apply H.
apply (trans_neg_trans HT); apply H.
apply (neg_trans_trans HT); [apply asym_antisym |]; apply H.
Qed.

Lemma strict_total_order_strict_weak_order :
   {R : T T Prop},
    eq_dec T strict_total_order R strict_weak_order R.
Proof. intros R HT; rewrite strict_total_order_equiv_swo; easy. Qed.

End Homogeneous_binary_relation_Facts3.

Section Homogeneous_binary_relation_Facts4a.

Compatibility results of elementary properties of homogeneous binary relations with operators.

Context {T : Type}.

With the converse / complementary / conv_compl operators.

Lemma conv_refl :
   {R : T T Prop}, reflexive R reflexive (converse R).
Proof. easy. Qed.

Lemma conv_refl_equiv :
   {R : T T Prop}, reflexive (converse R) reflexive R.
Proof. easy. Qed.

Lemma conv_irrefl :
   {R : T T Prop}, irreflexive R irreflexive (converse R).
Proof. easy. Qed.

Lemma conv_irrefl_equiv :
   {R : T T Prop}, irreflexive (converse R) irreflexive R.
Proof. easy. Qed.

Lemma conv_sym :
   {R : T T Prop}, symmetric R symmetric (converse R).
Proof. intros R H x y; apply (H y x). Qed.

Lemma conv_sym_equiv :
   {R : T T Prop}, symmetric (converse R) symmetric R.
Proof. intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_sym. Qed.

Lemma conv_antisym :
   {R : T T Prop}, antisymmetric R antisymmetric (converse R).
Proof. intros R H x; auto. Qed.

Lemma conv_antisym_equiv :
   {R : T T Prop}, antisymmetric (converse R) antisymmetric R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_antisym.
Qed.

Lemma conv_asym :
   {R : T T Prop}, asymmetric R asymmetric (converse R).
Proof. intros R H x y H1 H2; apply (H _ _ H2 H1). Qed.

Lemma conv_asym_equiv :
   {R : T T Prop}, asymmetric (converse R) asymmetric R.
Proof. intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_asym. Qed.

Lemma conv_trans :
   {R : T T Prop}, transitive R transitive (converse R).
Proof. intros R H x y z H1 H2; apply (H _ _ _ H2 H1). Qed.

Lemma conv_trans_equiv :
   {R : T T Prop}, transitive (converse R) transitive R.
Proof. intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_trans. Qed.

Lemma conv_neg_trans :
   {R : T T Prop},
    negatively_transitive R negatively_transitive (converse R).
Proof. intros R H x y z H1 H2; apply (H _ _ _ H2 H1). Qed.

Lemma conv_neg_trans_equiv :
   {R : T T Prop},
    negatively_transitive (converse R) negatively_transitive R.
Proof. intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_trans. Qed.

Lemma conv_conn :
   {R : T T Prop}, connected R connected (converse R).
Proof. intros R H x y; rewrite eq_sym_equiv; apply H. Qed.

Lemma conv_conn_equiv :
   {R : T T Prop}, connected (converse R) connected R.
Proof. intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_conn. Qed.

Lemma conv_str_conn :
   {R : T T Prop},
    strongly_connected R strongly_connected (converse R).
Proof. intros R H x y; apply (H y x). Qed.

Lemma conv_str_conn_equiv :
   {R : T T Prop},
    strongly_connected (converse R) strongly_connected R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_str_conn.
Qed.

Lemma conv_tricho :
   {R : T T Prop}, trichotomous R trichotomous (converse R).
Proof. intros R H x y; rewrite eq_sym_equiv; apply (H y x). Qed.

Lemma conv_tricho_equiv :
   {R : T T Prop}, trichotomous (converse R) trichotomous R.
Proof. intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_tricho. Qed.

Lemma compl_refl_equiv :
   {R : T T Prop}, reflexive (complementary R) irreflexive R.
Proof. easy. Qed.

Lemma compl_irrefl_equiv :
   {R : T T Prop}, irreflexive (complementary R) reflexive R.
Proof. intros; rewrite -compl_refl_equiv br_compl_invol; easy. Qed.

Lemma compl_sym :
   {R : T T Prop}, symmetric R symmetric (complementary R).
Proof. intros R H x y; rewrite -contra_equiv; apply H. Qed.

Lemma compl_sym_equiv :
   {R : T T Prop}, symmetric (complementary R) symmetric R.
Proof. intros R; split; [rewrite -{2}(br_compl_invol R) |]; apply compl_sym. Qed.

Lemma compl_antisym_equiv :
   {R : T T Prop}, antisymmetric (complementary R) connected R.
Proof. intros; apply iff_sym, conn_equiv_antisym. Qed.

Lemma compl_asym_equiv :
   {R : T T Prop},
    eq_dec T asymmetric (complementary R) strongly_connected R.
Proof.
intros R HT; rewrite asym_equiv_irrefl_antisym (str_conn_equiv_refl_conn HT).
apply and_iff_compat; [apply compl_irrefl_equiv | apply compl_antisym_equiv].
Qed.

Lemma compl_trans :
   {R : T T Prop},
    eq_dec T connected R transitive R transitive (complementary R).
Proof. intro; apply trans_neg_trans. Qed.

Lemma compl_neg_trans :
   {R : T T Prop},
    eq_dec T antisymmetric R
    negatively_transitive R negatively_transitive (complementary R).
Proof. intros; rewrite -trans_equiv; apply neg_trans_trans; easy. Qed.

Lemma compl_trans_equiv :
   {R : T T Prop},
    eq_dec T antisymmetric R connected R
    transitive (complementary R) transitive R.
Proof.
intros; split.
rewrite -neg_trans_equiv trans_equiv; apply compl_neg_trans; easy.
apply compl_trans; easy.
Qed.

Lemma compl_neg_trans_equiv :
   {R : T T Prop},
    eq_dec T antisymmetric R connected R
    negatively_transitive (complementary R) negatively_transitive R.
Proof.
intros; rewrite !neg_trans_equiv br_compl_invol;
    apply iff_sym, compl_trans_equiv; easy.
Qed.

Lemma compl_conn_equiv :
   {R : T T Prop}, connected (complementary R) antisymmetric R.
Proof. intros; apply iff_sym, antisym_equiv_conn. Qed.

Lemma compl_str_conn_equiv :
   {R : T T Prop},
    eq_dec T strongly_connected (complementary R) asymmetric R.
Proof. intros; rewrite -{2}(br_compl_invol R) compl_asym_equiv; easy. Qed.

Lemma compl_tricho_equiv :
   {R : T T Prop}, eq_dec T
    trichotomous (complementary R) antisymmetric R strongly_connected R.
Proof.
intros R HT; rewrite -compl_conn_equiv -(compl_asym_equiv HT) and_comm.
apply (tricho_equiv_asym_conn HT).
Qed.

Lemma total_order_equiv_tricho :
   {R : T T Prop},
    eq_dec T total_order R
    reflexive R transitive R trichotomous (complementary R).
Proof.
intros R HT; rewrite (compl_tricho_equiv HT); unfold total_order; tauto.
Qed.

Lemma total_order_equiv_pro_tricho :
   {R : T T Prop},
    eq_dec T total_order R preorder R trichotomous (complementary R).
Proof. intros R HT; rewrite (total_order_equiv_tricho HT) and_assoc; easy. Qed.

Lemma conv_compl_refl_equiv :
   {R : T T Prop}, reflexive (conv_compl R) irreflexive R.
Proof. easy. Qed.

Lemma conv_compl_irrefl_equiv :
   {R : T T Prop}, irreflexive (conv_compl R) reflexive R.
Proof. intros; rewrite conv_irrefl_equiv compl_irrefl_equiv; easy. Qed.

Lemma conv_compl_sym_equiv :
   {R : T T Prop}, symmetric (conv_compl R) symmetric R.
Proof. intros; rewrite conv_sym_equiv compl_sym_equiv; easy. Qed.

Lemma conv_compl_antisym_equiv :
   {R : T T Prop}, antisymmetric (conv_compl R) connected R.
Proof. intros; rewrite conv_antisym_equiv compl_antisym_equiv; easy. Qed.

Lemma conv_compl_asym_equiv :
   {R : T T Prop},
    eq_dec T asymmetric (conv_compl R) strongly_connected R.
Proof. intros; rewrite conv_asym_equiv compl_asym_equiv; easy. Qed.

Lemma conv_compl_trans :
   {R : T T Prop},
    eq_dec T connected R transitive R transitive (conv_compl R).
Proof. intros; apply conv_trans_equiv, compl_trans; easy. Qed.

Lemma conv_compl_neg_trans :
   {R : T T Prop},
    eq_dec T antisymmetric R
    negatively_transitive R negatively_transitive (conv_compl R).
Proof. intros; apply conv_neg_trans_equiv, compl_neg_trans; easy. Qed.

Lemma conv_compl_trans_equiv :
   {R : T T Prop},
    eq_dec T antisymmetric R connected R
    transitive (conv_compl R) transitive R.
Proof. intros; rewrite conv_trans_equiv compl_trans_equiv; easy. Qed.

Lemma conv_compl_neg_trans_equiv :
   {R : T T Prop},
    eq_dec T antisymmetric R connected R
    negatively_transitive (conv_compl R) negatively_transitive R.
Proof. intros; rewrite conv_neg_trans_equiv compl_neg_trans_equiv; easy. Qed.

Lemma conv_compl_conn_equiv :
   {R : T T Prop}, connected (conv_compl R) antisymmetric R.
Proof. intros; rewrite conv_conn_equiv compl_conn_equiv; easy. Qed.

Lemma conv_compl_str_conn_equiv :
   {R : T T Prop},
    eq_dec T strongly_connected (conv_compl R) asymmetric R.
Proof. intros; rewrite conv_str_conn_equiv compl_str_conn_equiv; easy. Qed.

Lemma conv_compl_tricho_equiv :
   {R : T T Prop}, eq_dec T
    trichotomous (conv_compl R) antisymmetric R strongly_connected R.
Proof. intros; rewrite conv_tricho_equiv compl_tricho_equiv; easy. Qed.

With the br_and / br_or operators.

Lemma br_and_refl :
   (R1 R2 : T T Prop),
    reflexive R1 reflexive R2 reflexive (br_and R1 R2).
Proof. easy. Qed.

Lemma br_and_refl_equiv :
   {R1 R2 : T T Prop},
    reflexive (br_and R1 R2) reflexive R1 reflexive R2.
Proof. intros; split; intros H; [split; intros x; apply H | easy]. Qed.

Lemma br_and_irrefl :
   (R1 R2 : T T Prop),
    irreflexive R1 irreflexive R2 irreflexive (br_and R1 R2).
Proof.
intros R1 R2 [H | H] x; rewrite not_and_equiv; [left | right]; easy.
Qed.

Lemma br_or_refl :
   (R1 R2 : T T Prop),
    reflexive R1 reflexive R2 reflexive (br_or R1 R2).
Proof. intros R1 R2 [H | H] x; [left | right]; easy. Qed.

A reflexive conjunction br_and R1 R2 does not mean that either R1 or R2 is reflexive, and similarly for an irreflexive disjunction. Thus, there is equivalence result neither for reflexive conjunctions, nor for irreflexive disjunctions.

Lemma br_or_irrefl :
   (R1 R2 : T T Prop),
    irreflexive R1 irreflexive R2 irreflexive (br_or R1 R2).
Proof. intros R1 R2 H1 H2 x; rewrite not_or_equiv; easy. Qed.

Lemma br_or_irrefl_equiv :
   {R1 R2 : T T Prop},
    irreflexive (br_or R1 R2) irreflexive R1 irreflexive R2.
Proof.
intros; split; [| intros; apply br_or_irrefl; easy].
intros H; split; intros x; specialize (H x); rewrite not_or_equiv in H; easy.
Qed.

Lemma br_and_sym :
   (R1 R2 : T T Prop),
    symmetric R1 symmetric R2 symmetric (br_and R1 R2).
Proof. intros R1 R2 H1 H2 x y [H3 H4]; split; [apply H1 | apply H2]; easy. Qed.

Lemma br_or_sym :
   (R1 R2 : T T Prop),
    symmetric R1 symmetric R2 symmetric (br_or R1 R2).
Proof.
intros R1 R2 H1 H2 x y [H3 | H3]; [left; apply H1 | right; apply H2]; easy.
Qed.

Lemma br_and_antisym :
   (R1 R2 : T T Prop),
    antisymmetric R1 antisymmetric R2 antisymmetric (br_and R1 R2).
Proof. intros R1 R2 [H | H] x y [H1 H2] [H3 H4]; apply (H x y); easy. Qed.

Lemma br_and_asym :
   (R1 R2 : T T Prop),
    asymmetric R1 asymmetric R2 asymmetric (br_and R1 R2).
Proof. intros R1 R2 [H | H] x y [H1 H2] [H3 H4]; apply (H x y); easy. Qed.

Lemma br_and_trans :
   (R1 R2 : T T Prop),
    transitive R1 transitive R2 transitive (br_and R1 R2).
Proof.
intros R1 R2 H1 H2 x y z [H3 H4] [H5 H6]; split;
    [apply H1 with y | apply H2 with y]; easy.
Qed.

Lemma br_or_neg_trans :
   (R1 R2 : T T Prop),
    negatively_transitive R1 negatively_transitive R2
    negatively_transitive (br_or R1 R2).
Proof.
intros R1 R2 H1 H2 x y z; rewrite !not_or_equiv; intros [H3 H4] [H5 H6]; split;
    [apply H1 with y | apply H2 with y]; easy.
Qed.

Lemma br_or_conn :
   (R1 R2 : T T Prop),
    connected R1 connected R2 connected (br_or R1 R2).
Proof.
intros R1 R2 [H | H] x y H1; destruct (H _ _ H1) as [H2 | H2];
    [left; left | right; left | left; right | right; right]; easy.
Qed.

Lemma br_or_str_conn :
   (R1 R2 : T T Prop),
    strongly_connected R1 strongly_connected R2
    strongly_connected (br_or R1 R2).
Proof.
intros R1 R2 [H | H] x y; destruct (H x y) as [H1 | H1];
    [left; left | right; left | left; right | right; right]; easy.
Qed.

With the br_and_neq / br_or_eq operators.

Lemma br_and_neq_irrefl :
   {R : T T Prop}, irreflexive (br_and_neq R).
Proof. intros; apply br_and_irrefl; left; easy. Qed.

Lemma br_and_neq_not_refl :
   {R : T T Prop}, inhabited T ¬ reflexive (br_and_neq R).
Proof. intros; apply irrefl_not_refl; [easy | apply br_and_neq_irrefl]. Qed.

Lemma br_or_eq_refl : {R : T T Prop}, reflexive (br_or_eq R).
Proof. intros; apply br_or_refl; left; easy. Qed.

Lemma br_or_eq_not_irrefl :
   {R : T T Prop}, inhabited T ¬ irreflexive (br_or_eq R).
Proof. intros; apply refl_not_irrefl; [easy | apply br_or_eq_refl]. Qed.

Lemma br_and_neq_sym :
   {R : T T Prop}, symmetric R symmetric (br_and_neq R).
Proof. intros; apply br_and_sym; [intros x y; apply not_eq_sym | easy]. Qed.

Lemma br_or_eq_sym :
   {R : T T Prop}, symmetric R symmetric (br_or_eq R).
Proof. intros; apply br_or_sym; easy. Qed.

Lemma br_and_neq_antisym :
   {R : T T Prop}, antisymmetric R antisymmetric (br_and_neq R).
Proof. intros; apply br_and_antisym; right; easy. Qed.

Lemma br_and_neq_asym :
   {R : T T Prop}, asymmetric R asymmetric (br_and_neq R).
Proof. intros; apply br_and_asym; right; easy. Qed.

Lemma br_or_eq_antisym :
   {R : T T Prop}, antisymmetric R antisymmetric (br_or_eq R).
Proof. intros R H x y [H1 | H1] [H2 | H2]; [..| apply H]; easy. Qed.

Lemma br_or_eq_antisym_rev :
   {R : T T Prop}, antisymmetric (br_or_eq R) antisymmetric R.
Proof. intros R H x y H1 H2; apply H; right; easy. Qed.

Lemma br_or_eq_antisym_equiv :
   {R : T T Prop}, antisymmetric (br_or_eq R) antisymmetric R.
Proof.
intros; split; [apply br_or_eq_antisym_rev | apply br_or_eq_antisym].
Qed.

Lemma br_or_eq_not_asym :
   {R : T T Prop}, inhabited T ¬ asymmetric (br_or_eq R).
Proof. intros; apply refl_not_asym; [easy | apply br_or_eq_refl]. Qed.

Lemma br_and_neq_trans :
   {R : T T Prop},
    antisymmetric R transitive R transitive (br_and_neq R).
Proof.
intros R H1 H2 x y z [H3a H3b] [H4a H4b]; split; [| apply H2 with y; easy].
contradict H3a; apply H1; [| rewrite H3a]; easy.
Qed.

Lemma br_or_eq_trans :
   {R : T T Prop}, transitive R transitive (br_or_eq R).
Proof.
intros R H x y z [H1 | H1] [H2 | H2]; subst;
    [left | right.. | right; apply H with y]; easy.
Qed.

Lemma br_and_neq_neg_trans :
   {R : T T Prop},
    negatively_transitive R negatively_transitive (br_and_neq R).
Proof.
intros R; rewrite !neg_trans_equiv -br_or_eq_compl; apply br_or_eq_trans.
Qed.

Lemma br_or_eq_neg_trans :
   {R : T T Prop},
    connected R
    negatively_transitive R negatively_transitive (br_or_eq R).
Proof.
intros R H1; rewrite !neg_trans_equiv -br_and_neq_compl.
apply br_and_neq_trans; rewrite compl_antisym_equiv; easy.
Qed.

Lemma br_and_neq_conn :
   {R : T T Prop}, connected R connected (br_and_neq R).
Proof.
intros R H x y H1; destruct (H _ _ H1) as [H2 | H2]; [left | right]; easy.
Qed.

Lemma br_and_neq_not_str_conn :
   {R : T T Prop},
    inhabited T ¬ strongly_connected (br_and_neq R).
Proof.
moveR /(@br_and_neq_not_refl R); rewrite -contra_equiv; apply str_conn_refl.
Qed.

Lemma br_or_eq_conn :
   {R : T T Prop}, connected R connected (br_or_eq R).
Proof. intros; apply br_or_conn; right; easy. Qed.

Lemma br_or_eq_str_conn :
   {R : T T Prop},
    strongly_connected R strongly_connected (br_or_eq R).
Proof. intros; apply br_or_str_conn; right; easy. Qed.

Lemma br_and_neq_tricho :
   {R : T T Prop}, trichotomous R trichotomous (br_and_neq R).
Proof.
intros R H x y; destruct (H x y) as [H1 | [H1 | H1]].
left; rewrite !not_and_equiv; repeat split; [| right..]; easy.
right; left; rewrite not_and_equiv; repeat split; [..| right]; easy.
right; right; rewrite not_and_equiv; repeat split; [..| right]; easy.
Qed.

Lemma br_or_eq_not_tricho :
   {R : T T Prop},
    inhabited T eq_dec T ¬ trichotomous (br_or_eq R).
Proof.
intros; rewrite tricho_equiv_asym_conn// not_and_equiv;
    left; apply br_or_eq_not_asym; easy.
Qed.

With the strict / equivalent operators.

Lemma strict_asym : (R : T T Prop), asymmetric (strict R).
Proof. intros R x y [H1 _] [_ H2]; easy. Qed.

Lemma strict_irrefl : (R : T T Prop), irreflexive (strict R).
Proof. intros; apply asym_irrefl, strict_asym. Qed.

Lemma strict_antisym : (R : T T Prop), antisymmetric (strict R).
Proof. intros; apply asym_antisym, strict_asym. Qed.

Lemma strict_trans :
   {R : T T Prop},
    transitive R negatively_transitive R transitive (strict R).
Proof. intros; apply br_and_trans; [| apply conv_trans]; easy. Qed.

Lemma strict_conn :
   {R : T T Prop},
    antisymmetric R connected R connected (strict R).
Proof.
intros R H1 H2 x y H3; destruct (H2 _ _ H3) as [H4 | H4];
    [left | right]; (split; [| contradict H3; apply H1]); easy.
Qed.

Lemma equivalent_refl :
   {R : T T Prop}, reflexive R reflexive (equivalent R).
Proof. intros; apply br_and_refl; [| apply conv_refl]; easy. Qed.

Lemma equivalent_sym : (R : T T Prop), symmetric (equivalent R).
Proof. intros R x y H; split; apply H. Qed.

Lemma equivalent_trans :
   {R : T T Prop}, transitive R transitive (equivalent R).
Proof. intros; apply br_and_trans; [| apply conv_trans]; easy. Qed.

With the comparable / incomparable operators.

Lemma compar_refl_equiv :
   {R : T T Prop}, reflexive (comparable R) reflexive R.
Proof. intros; split; intros H x; [destruct (H x) | left]; easy. Qed.

Lemma incompar_refl_equiv :
   {R : T T Prop}, reflexive (incomparable R) irreflexive R.
Proof. unfold incomparable; intros; split; [intros H x; apply H | easy]. Qed.

Lemma incompar_irrefl_equiv :
   {R : T T Prop},
    irreflexive (incomparable R) irreflexive (complementary R).
Proof.
intros; rewrite -!compl_refl_equiv compl_incompar br_compl_invol;
    apply compar_refl_equiv.
Qed.

Lemma compar_irrefl_equiv :
   {R : T T Prop},
    irreflexive (comparable R) reflexive (complementary R).
Proof.
intros; rewrite -incompar_refl_equiv incompar_compar
    compl_refl_equiv incompar_refl_equiv; easy.
Qed.

Lemma compar_sym : (R : T T Prop), symmetric (comparable R).
Proof. unfold comparable; intros R1 x y H; rewrite or_comm; easy. Qed.

Lemma incompar_sym : (R : T T Prop), symmetric (incomparable R).
Proof. unfold incomparable; intros R1 x y H; rewrite and_comm; easy. Qed.

Lemma incompar_trans :
   {R : T T Prop},
    negatively_transitive R transitive (incomparable R).
Proof. intros; apply br_and_trans; [| apply conv_trans]; easy. Qed.

Lemma incompar_compl_trans :
   {R : T T Prop},
    transitive R transitive (incomparable (complementary R)).
Proof.
intros; apply incompar_trans, neg_trans_equiv; rewrite br_compl_invol; easy.
Qed.

End Homogeneous_binary_relation_Facts4a.

Section Homogeneous_binary_relation_Facts4b.

Compatibility results of compound properties of homogeneous binary relations with operators.

Context {T : Type}.

With the converse / complementary / conv_compl operators.

Lemma conv_partial_equiv_rel :
   {R : T T Prop},
    partial_equivalence_relation R
    partial_equivalence_relation (converse R).
Proof. intro; apply modus_ponens_and; [apply conv_sym | apply conv_trans]. Qed.

Lemma conv_partial_equiv_rel_equiv :
   {R : T T Prop},
    partial_equivalence_relation (converse R)
    partial_equivalence_relation R.
Proof.
intro; split; [rewrite -{2}(conv_invol R) |]; apply conv_partial_equiv_rel.
Qed.

Lemma conv_equiv_rel :
   {R : T T Prop},
    equivalence_relation R equivalence_relation (converse R).
Proof.
intro; rewrite !equiv_rel_equiv_per; apply modus_ponens_and;
    [apply conv_partial_equiv_rel | apply conv_refl].
Qed.

Lemma conv_equiv_rel_equiv :
   {R : T T Prop},
    equivalence_relation (converse R) equivalence_relation R.
Proof. intro; split; [rewrite -{2}(conv_invol R) |]; apply conv_equiv_rel. Qed.

Lemma conv_preorder :
   {R : T T Prop}, preorder R preorder (converse R).
Proof.
intro; apply modus_ponens_and; [apply conv_refl | apply conv_trans].
Qed.

Lemma conv_preorder_equiv :
   {R : T T Prop}, preorder (converse R) preorder R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_preorder.
Qed.

Lemma conv_total_preorder :
   {R : T T Prop},
    eq_dec T total_preorder R total_preorder (converse R).
Proof.
intros R HT; rewrite !(total_preorder_equiv_pro HT); apply modus_ponens_and;
    [apply conv_preorder | apply conv_conn].
Qed.

Lemma conv_total_preorder_equiv :
   {R : T T Prop},
    eq_dec T total_preorder (converse R) total_preorder R.
Proof.
intros R HT; split;
    [rewrite -{2}(conv_invol R) |]; apply (conv_total_preorder HT).
Qed.

Lemma conv_partial_order :
   {R : T T Prop}, partial_order R partial_order (converse R).
Proof.
intro; rewrite !partial_order_equiv; apply modus_ponens_and;
    [apply conv_preorder | apply conv_antisym].
Qed.

Lemma conv_partial_order_equiv :
   {R : T T Prop}, partial_order (converse R) partial_order R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_partial_order.
Qed.

Lemma conv_total_order :
   {R : T T Prop},
    eq_dec T total_order R total_order (converse R).
Proof.
intros R HT; rewrite !(total_order_equiv_po HT); apply modus_ponens_and;
    [apply conv_partial_order | apply conv_conn].
Qed.

Lemma conv_total_order_equiv :
   {R : T T Prop},
    eq_dec T total_order (converse R) total_order R.
Proof.
intros R HT; split;
    [rewrite -{2}(conv_invol R) |]; apply (conv_total_order HT).
Qed.

Lemma conv_strict_partial_order :
   {R : T T Prop},
    strict_partial_order R strict_partial_order (converse R).
Proof.
intro; rewrite !strict_partial_order_equiv_no_asym; apply modus_ponens_and;
    [apply conv_irrefl | apply conv_trans].
Qed.

Lemma conv_strict_partial_order_equiv :
   {R : T T Prop},
    strict_partial_order (converse R) strict_partial_order R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |];
    apply conv_strict_partial_order.
Qed.

Lemma conv_strict_total_order :
   {R : T T Prop},
    strict_total_order R strict_total_order (converse R).
Proof.
intro; rewrite !strict_total_order_equiv_spo; apply modus_ponens_and;
    [apply conv_strict_partial_order | apply conv_conn].
Qed.

Lemma conv_strict_total_order_equiv :
   {R : T T Prop},
    strict_total_order (converse R) strict_total_order R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_strict_total_order.
Qed.

Lemma conv_strict_weak_order :
   {R : T T Prop},
    strict_weak_order R strict_weak_order (converse R).
Proof.
intro; rewrite !strict_weak_order_equiv; apply modus_ponens_and;
    [apply conv_asym | apply conv_neg_trans].
Qed.

Lemma conv_strict_weak_order_equiv :
   {R : T T Prop},
    strict_weak_order (converse R) strict_weak_order R.
Proof.
intros R; split; [rewrite -{2}(conv_invol R) |]; apply conv_strict_weak_order.
Qed.

Lemma compl_partial_equiv_rel :
   {R : T T Prop},
    eq_dec T connected R
    partial_equivalence_relation R
    partial_equivalence_relation (complementary R).
Proof.
intros R HT H1 H2; split; [apply compl_sym | apply compl_trans];
    [apply H2 | easy.. | apply H2].
Qed.

Lemma compl_partial_equiv_rel_equiv :
   {R : T T Prop},
    eq_dec T antisymmetric R connected R
    partial_equivalence_relation (complementary R)
    partial_equivalence_relation R.
Proof.
moveR HT /compl_conn_equiv H1 H2; split;
    [rewrite -{2}(br_compl_invol R) |]; apply compl_partial_equiv_rel; easy.
Qed.

Lemma compl_equiv_rel :
   {R : T T Prop},
    irreflexive R symmetric R negatively_transitive R
    equivalence_relation (complementary R).
Proof.
intros; repeat split; [apply compl_refl_equiv | apply compl_sym |]; easy.
Qed.

Lemma compl_equiv_rel_equiv :
   {R : T T Prop},
    equivalence_relation (complementary R)
    irreflexive R symmetric R negatively_transitive R.
Proof.
intros; split; intros H; [| apply compl_equiv_rel; easy].
repeat split; [rewrite -compl_refl_equiv | apply compl_sym_equiv | ]; apply H.
Qed.

Lemma compl_preorder_equiv :
   {R : T T Prop},
    preorder (complementary R) irreflexive R negatively_transitive R.
Proof. intros; rewrite -compl_refl_equiv; easy. Qed.

Lemma compl_total_preorder :
   {R : T T Prop},
    eq_dec T strict_weak_order R total_preorder (complementary R).
Proof.
intros R HT H; repeat split;
    [apply compl_refl_equiv | | apply (compl_str_conn_equiv HT)]; apply H.
Qed.

Lemma compl_strict_weak_order :
   {R : T T Prop},
    eq_dec T total_preorder R strict_weak_order (complementary R).
Proof.
intros R HT H; repeat split;
    [apply compl_irrefl_equiv | apply (compl_asym_equiv HT) |
    rewrite -trans_equiv]; apply H.
Qed.

Lemma compl_total_preorder_equiv :
   {R : T T Prop},
    eq_dec T total_preorder (complementary R) strict_weak_order R.
Proof.
intros R HT; split; [rewrite -{2}(br_compl_invol R);
    apply (compl_strict_weak_order HT) | apply (compl_total_preorder HT)].
Qed.

Lemma compl_strict_weak_order_equiv :
   {R : T T Prop},
    eq_dec T strict_weak_order (complementary R) total_preorder R.
Proof.
intros R HT; rewrite -{2}(br_compl_invol R);
    apply iff_sym, (compl_total_preorder_equiv HT).
Qed.

Lemma compl_partial_order_equiv :
   {R : T T Prop},
    partial_order (complementary R)
    irreflexive R negatively_transitive R connected R.
Proof.
intros; rewrite partial_order_equiv compl_preorder_equiv
    compl_antisym_equiv; tauto.
Qed.

Lemma compl_total_order :
   {R : T T Prop},
    eq_dec T strict_total_order R total_order (complementary R).
Proof.
intros R HT H; repeat split;
    [apply compl_refl_equiv | apply compl_antisym_equiv |
    apply (trans_neg_trans HT) | apply (compl_str_conn_equiv HT)]; apply H.
Qed.

Lemma compl_strict_total_order :
   {R : T T Prop},
    eq_dec T total_order R strict_total_order (complementary R).
Proof.
intros R HT H; repeat split;
    [apply compl_irrefl_equiv | rewrite (compl_asym_equiv HT) |
    apply (trans_neg_trans HT); [apply str_conn_conn |] |
    apply compl_conn_equiv]; apply H.
Qed.

Lemma compl_total_order_equiv :
   {R : T T Prop},
    eq_dec T total_order (complementary R) strict_total_order R.
Proof.
intros R HT; split; [rewrite -{2}(br_compl_invol R);
    apply (compl_strict_total_order HT) | apply (compl_total_order HT)].
Qed.

Lemma compl_strict_total_order_equiv :
   {R : T T Prop},
    eq_dec T strict_total_order (complementary R) total_order R.
Proof.
intros R HT; rewrite -{2}(br_compl_invol R);
    apply iff_sym, (compl_total_order_equiv HT).
Qed.

Lemma compl_strict_partial_order_equiv :
   {R : T T Prop},
    eq_dec T strict_partial_order (complementary R)
    reflexive R negatively_transitive R strongly_connected R.
Proof.
intros R HT; rewrite -compl_irrefl_equiv -(compl_asym_equiv HT);
    unfold strict_partial_order; tauto.
Qed.

Lemma conv_compl_partial_equiv_rel :
   {R : T T Prop},
    eq_dec T connected R
    partial_equivalence_relation R
    partial_equivalence_relation (conv_compl R).
Proof.
intros; apply conv_partial_equiv_rel, compl_partial_equiv_rel; easy.
Qed.

Lemma conv_compl_partial_equiv_rel_equiv :
   {R : T T Prop},
    eq_dec T antisymmetric R connected R
    partial_equivalence_relation (conv_compl R)
    partial_equivalence_relation R.
Proof.
intros; rewrite conv_partial_equiv_rel_equiv
    compl_partial_equiv_rel_equiv; easy.
Qed.

Lemma conv_compl_equiv_rel :
   {R : T T Prop},
    irreflexive R symmetric R negatively_transitive R
    equivalence_relation (conv_compl R).
Proof. intros; apply conv_equiv_rel, compl_equiv_rel; easy. Qed.

Lemma conv_compl_equiv_rel_equiv :
   {R : T T Prop},
    equivalence_relation (conv_compl R)
    irreflexive R symmetric R negatively_transitive R.
Proof. intros; rewrite conv_equiv_rel_equiv compl_equiv_rel_equiv; easy. Qed.

Lemma conv_compl_preorder_equiv :
   {R : T T Prop},
    preorder (conv_compl R) irreflexive R negatively_transitive R.
Proof. intros; rewrite conv_preorder_equiv compl_preorder_equiv; easy. Qed.

Lemma conv_compl_total_preorder :
   {R : T T Prop},
    eq_dec T strict_weak_order R total_preorder (conv_compl R).
Proof. intros; apply conv_total_preorder, compl_total_preorder; easy. Qed.

Lemma conv_compl_strict_weak_order :
   {R : T T Prop},
    eq_dec T total_preorder R strict_weak_order (conv_compl R).
Proof.
intros; apply conv_strict_weak_order, compl_strict_weak_order; easy.
Qed.

Lemma conv_compl_total_preorder_equiv :
   {R : T T Prop},
    eq_dec T total_preorder (conv_compl R) strict_weak_order R.
Proof.
intros R HT; rewrite (conv_total_preorder_equiv HT)
    compl_total_preorder_equiv; easy.
Qed.

Lemma conv_compl_strict_weak_order_equiv :
   {R : T T Prop},
    eq_dec T strict_weak_order (conv_compl R) total_preorder R.
Proof.
intros; rewrite conv_strict_weak_order_equiv
    compl_strict_weak_order_equiv; easy.
Qed.

Lemma conv_compl_partial_order_equiv :
   {R : T T Prop},
    partial_order (conv_compl R)
    irreflexive R negatively_transitive R connected R.
Proof.
intros; rewrite conv_partial_order_equiv compl_partial_order_equiv; easy.
Qed.

Lemma conv_compl_total_order :
   {R : T T Prop},
    eq_dec T strict_total_order R total_order (conv_compl R).
Proof. intros; apply conv_total_order, compl_total_order; easy. Qed.

Lemma conv_compl_strict_total_order :
   {R : T T Prop},
    eq_dec T total_order R strict_total_order (conv_compl R).
Proof.
intros; apply conv_strict_total_order, compl_strict_total_order; easy.
Qed.

Lemma conv_compl_total_order_equiv :
   {R : T T Prop},
    eq_dec T total_order (conv_compl R) strict_total_order R.
Proof.
intros R HT; rewrite (conv_total_order_equiv HT) compl_total_order_equiv; easy.
Qed.

Lemma conv_compl_strict_total_order_equiv :
   {R : T T Prop},
    eq_dec T strict_total_order (conv_compl R) total_order R.
Proof.
intros; rewrite conv_strict_total_order_equiv
    compl_strict_total_order_equiv; easy.
Qed.

Lemma conv_compl_strict_partial_order_equiv :
   {R : T T Prop},
    eq_dec T strict_partial_order (conv_compl R)
    reflexive R negatively_transitive R strongly_connected R.
Proof.
intros; rewrite conv_strict_partial_order_equiv
    compl_strict_partial_order_equiv; easy.
Qed.

With the br_and / br_or operators.

Lemma br_and_partial_equiv_rel :
   (R1 R2 : T T Prop),
    partial_equivalence_relation R1 partial_equivalence_relation R2
    partial_equivalence_relation (br_and R1 R2).
Proof.
intros R1 R2; apply modus_ponens_and3; [apply br_and_sym | apply br_and_trans].
Qed.

Lemma br_and_equiv_rel :
   (R1 R2 : T T Prop),
    equivalence_relation R1 equivalence_relation R2
    equivalence_relation (br_and R1 R2).
Proof.
intros R1 R2; rewrite !equiv_rel_equiv_per; apply modus_ponens_and3;
    [apply br_and_partial_equiv_rel | apply br_and_refl].
Qed.

Lemma br_and_preorder :
   (R1 R2 : T T Prop),
    preorder R1 preorder R2 preorder (br_and R1 R2).
Proof.
intros R1 R2; apply modus_ponens_and3;
    [apply br_and_refl | apply br_and_trans].
Qed.

Lemma br_and_partial_order :
   (R1 R2 : T T Prop),
    partial_order R1 partial_order R2 partial_order (br_and R1 R2).
Proof.
intros R1 R2; rewrite !partial_order_equiv; apply modus_ponens_and3;
    [apply br_and_preorder | intros; apply br_and_antisym; left; easy].
Qed.

Lemma br_and_strict_partial_order :
   (R1 R2 : T T Prop),
    strict_partial_order R1 strict_partial_order R2
    strict_partial_order (br_and R1 R2).
Proof.
intros R1 R2; rewrite !strict_partial_order_equiv_no_asym;
    apply modus_ponens_and3;
    [intros; apply br_and_irrefl; left; easy | apply br_and_trans].
Qed.

With the br_and_neq / br_or_eq operators.

Lemma br_or_eq_partial_equiv_rel :
   {R : T T Prop},
    partial_equivalence_relation R
    partial_equivalence_relation (br_or_eq R).
Proof.
intro; apply modus_ponens_and; [apply br_or_eq_sym | apply br_or_eq_trans].
Qed.

Lemma br_or_eq_equiv_rel :
   {R : T T Prop},
    partial_equivalence_relation R equivalence_relation (br_or_eq R).
Proof.
intros; rewrite equiv_rel_equiv_per; split;
    [apply br_or_eq_partial_equiv_rel; easy | apply br_or_eq_refl].
Qed.

Lemma br_or_eq_preorder :
   {R : T T Prop}, transitive R preorder (br_or_eq R).
Proof. intros; split; [apply br_or_eq_refl | apply br_or_eq_trans; easy]. Qed.

Lemma br_or_eq_total_preorder :
   {R : T T Prop},
    eq_dec T total_preorder R total_preorder (br_or_eq R).
Proof.
intros R HT; rewrite !(total_preorder_equiv_pro HT); apply modus_ponens_and;
    [intros H; apply br_or_eq_preorder, H | apply br_or_eq_conn].
Qed.

Lemma br_or_eq_partial_order :
   {R : T T Prop}, partial_order R partial_order (br_or_eq R).
Proof.
intro; rewrite !partial_order_equiv; apply modus_ponens_and;
    [intros H; apply br_or_eq_preorder, H | apply br_or_eq_antisym].
Qed.

"spo" stands for "strict_partial_order".
Lemma br_or_eq_partial_order_spo :
   {R : T T Prop},
    strict_partial_order R partial_order (br_or_eq R).
Proof.
intros R H; rewrite !partial_order_equiv; split;
    [apply br_or_eq_preorder, H | apply br_or_eq_antisym, asym_antisym, H].
Qed.

Lemma br_or_eq_total_order :
   {R : T T Prop},
    eq_dec T total_order R total_order (br_or_eq R).
Proof.
intros R HT; rewrite !total_order_equiv_tpro; apply modus_ponens_and;
    [apply (br_or_eq_total_preorder HT) | apply br_or_eq_antisym].
Qed.

"sto" stands for "strict_total_order".
Lemma br_or_eq_total_order_sto :
   {R : T T Prop},
    eq_dec T strict_total_order R total_order (br_or_eq R).
Proof.
intros R HT; rewrite strict_total_order_equiv_spo (total_order_equiv_po HT);
    apply modus_ponens_and;
    [apply br_or_eq_partial_order_spo | apply br_or_eq_conn].
Qed.

Lemma br_and_neq_strict_partial_order :
   {R : T T Prop},
    strict_partial_order R strict_partial_order (br_and_neq R).
Proof.
intros R H; rewrite strict_partial_order_equiv_no_irrefl; split.
apply br_and_neq_asym, H.
apply br_and_neq_trans; [apply asym_antisym |]; apply H.
Qed.

Lemma br_and_neq_strict_total_order :
   {R : T T Prop},
    strict_total_order R strict_total_order (br_and_neq R).
Proof.
intros R; rewrite !strict_total_order_equiv_spo; apply modus_ponens_and.
apply br_and_neq_strict_partial_order.
apply br_and_neq_conn.
Qed.

Lemma br_and_neq_strict_weak_order :
   {R : T T Prop},
    strict_weak_order R strict_weak_order (br_and_neq R).
Proof.
intros R; rewrite !strict_weak_order_equiv; apply modus_ponens_and;
    [apply br_and_neq_asym | apply br_and_neq_neg_trans].
Qed.

With the strict / equivalent operators.

Lemma strict_strict_partial_order :
   {R : T T Prop},
    transitive R negatively_transitive R strict_partial_order (strict R).
Proof.
intros; rewrite strict_partial_order_equiv_no_asym; split;
    [apply strict_irrefl | apply strict_trans; easy].
Qed.

Lemma strict_strict_total_order :
   {R : T T Prop},
    eq_dec T antisymmetric R transitive R connected R
    strict_total_order (strict R).
Proof.
intros; apply strict_total_order_equiv_spo; split;
    [apply strict_strict_partial_order | apply strict_conn]; try easy.
apply trans_neg_trans; easy.
Qed.

"to" stands for "total_order".
Lemma strict_strict_total_order_to :
   {R : T T Prop},
    eq_dec T total_order R strict_total_order (strict R).
Proof.
intros R HT H; apply strict_strict_total_order;
    [easy |..| apply str_conn_conn]; apply H.
Qed.

Lemma equivalent_partial_equiv_rel :
   {R : T T Prop},
    preorder R partial_equivalence_relation (equivalent R).
Proof.
intros R H; split; [apply equivalent_sym | apply equivalent_trans, H].
Qed.

Lemma equivalent_equiv_rel :
   {R : T T Prop},
    preorder R equivalence_relation (equivalent R).
Proof.
intros; rewrite equiv_rel_equiv_per; split;
    [apply equivalent_partial_equiv_rel | apply equivalent_refl]; apply H.
Qed.

With the comparable / incomparable operators.

Lemma incompar_partial_equiv_rel :
   {R : T T Prop},
    irreflexive R negatively_transitive R
    partial_equivalence_relation (incomparable R).
Proof. intros; split; [apply incompar_sym | apply incompar_trans]; easy. Qed.

Lemma incompar_equiv_rel :
   {R : T T Prop},
    irreflexive R negatively_transitive R
    equivalence_relation (incomparable R).
Proof.
intros; rewrite equiv_rel_equiv_per; split;
    [apply incompar_partial_equiv_rel | apply incompar_refl_equiv]; easy.
Qed.

End Homogeneous_binary_relation_Facts4b.