Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders
  HoTT.Classes.theory.apartness.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]

Generalizable Variables A.

Lemma irrefl_neq `{R : Relation A} `{!Irreflexive R}
  : forall x y, R x y -> x <> y.
A: Type
R: Relation A
Irreflexive0: Irreflexive R
forall x y : A, R x y -> x <> y
Proof.
A: Type
R: Relation A
Irreflexive0: Irreflexive R
forall x y : A, R x y -> x <> y
intros ?? E e;rewrite e in E.
A: Type
R: Relation A
Irreflexive0: Irreflexive R
x, y: A
E: R y y
e: x = y
Empty exact (irreflexivity _ _ E).
Qed.

Lemma le_flip `{Le A} `{!TotalRelation (≤)} x y : ~(y ≤ x) -> x ≤ y.
A: Type
H: Le A
TotalRelation0: TotalRelation le
x, y: A
~ (y ≤ x) -> x ≤ y
Proof.
A: Type
H: Le A
TotalRelation0: TotalRelation le
x, y: A
~ (y ≤ x) -> x ≤ y
intros nle.
A: Type
H: Le A
TotalRelation0: TotalRelation le
x, y: A
nle: ~ (y ≤ x)
x ≤ y
destruct (total _ x y) as [?|le];auto.
A: Type
H: Le A
TotalRelation0: TotalRelation canonical_names.le
x, y: A
nle: ~ (y ≤ x)
le: y ≤ x
x ≤ y
destruct (nle le).
Qed.

Section partial_order.
  Context `{PartialOrder A}.

  Lemma eq_le x y : x = y -> x ≤ y.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
x = y -> x ≤ y
  Proof.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
x = y -> x ≤ y
  intros E.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E: x = y
x ≤ y
  rewrite E.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E: x = y
y ≤ y
  apply reflexivity.
  Qed.

  Lemma eq_le_flip x y : x = y -> y ≤ x.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
x = y -> y ≤ x
  Proof.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
x = y -> y ≤ x
  intros E.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E: x = y
y ≤ x
  rewrite E.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E: x = y
y ≤ y
  apply reflexivity.
  Qed.

  Lemma not_le_ne x y : ~(x ≤ y) -> x <> y.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
~ (x ≤ y) -> x <> y
  Proof.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
~ (x ≤ y) -> x <> y
  intros E1 E2.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E1: ~ (x ≤ y)
E2: x = y
Empty
  apply E1.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E1: ~ (x ≤ y)
E2: x = y
x ≤ y
  rewrite E2.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E1: ~ (x ≤ y)
E2: x = y
y ≤ y
  apply reflexivity.
  Qed.

  Lemma eq_iff_le x y : x = y <-> x ≤ y /\ y ≤ x.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
x = y <-> x ≤ y ≤ x
  Proof.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
x = y <-> x ≤ y ≤ x
  split; intros E.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E: x = y
x ≤ y ≤ x
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E: x ≤ y ≤ x
x = y
  -
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E: x = y
x ≤ y ≤ x rewrite E.
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E: x = y
y ≤ y ≤ y split;apply reflexivity.
  -
A: Type
Ale: Le A
H: PartialOrder Ale
x, y: A
E: x ≤ y ≤ x
x = y apply (antisymmetry (≤) x y);apply E.
  Qed.
End partial_order.

Section strict_order.
  Context `{StrictOrder A}.

  Lemma lt_flip x y : x < y -> ~(y < x).
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
x < y -> ~ (y < x)
  Proof.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
x < y -> ~ (y < x)
  intros E1 E2.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
E1: x < y
E2: y < x
Empty
  apply (irreflexivity (<) x).
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
E1: x < y
E2: y < x
x < x
  transitivity y;assumption.
  Qed.

  Lemma lt_antisym x y : ~(x < y < x).
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
~ (x < y < x)
  Proof.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
~ (x < y < x)
  intros [E1 E2].
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
E1: x < y
E2: y < x
Empty
  destruct (lt_flip x y);assumption.
  Qed.

  Lemma lt_ne x y : x < y -> x <> y.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
x < y -> x <> y
  Proof.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
x < y -> x <> y
  intros E1 E2.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
E1: x < y
E2: x = y
Empty
  rewrite E2 in E1.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
E1: y < y
E2: x = y
Empty
  apply (irreflexivity (<) y).
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
E1: y < y
E2: x = y
y < y assumption.
  Qed.

  Lemma lt_ne_flip x y : x < y -> y <> x.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
x < y -> y <> x
  Proof.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
x < y -> y <> x
  intro.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
X: x < y
y <> x
  apply symmetric_neq, lt_ne.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
X: x < y
x < y
  assumption.
  Qed.

  Lemma eq_not_lt x y : x = y -> ~(x < y).
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
x = y -> ~ (x < y)
  Proof.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
x = y -> ~ (x < y)
  intros E.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
E: x = y
~ (x < y)
  rewrite E.
A: Type
Alt: Lt A
H: StrictOrder Alt
x, y: A
E: x = y
~ (y < y)
  apply (irreflexivity (<)).
  Qed.
End strict_order.

Section pseudo_order.
  Context `{PseudoOrder A}.

  Local Existing Instance pseudo_order_apart.

  Lemma apart_total_lt x y : x ≶ y -> x < y |_| y < x.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
x ≶ y -> (x < y) + (y < x)
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
x ≶ y -> (x < y) + (y < x)
  intros.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
X: x ≶ y
((x < y) + (y < x))%type
  apply apart_iff_total_lt.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
X: x ≶ y
x ≶ y
  assumption.
  Qed.

  Lemma pseudo_order_lt_apart x y : x < y -> x ≶ y.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
x < y -> x ≶ y
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
x < y -> x ≶ y
  intros.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
X: x < y
x ≶ y
  apply apart_iff_total_lt.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
X: x < y
((x < y) + (y < x))%type
  auto.
  Qed.

  Lemma pseudo_order_lt_apart_flip x y : x < y -> y ≶ x.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
x < y -> y ≶ x
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
x < y -> y ≶ x
  intros.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
X: x < y
y ≶ x
  apply apart_iff_total_lt.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
X: x < y
((y < x) + (x < y))%type
  auto.
  Qed.

  Lemma not_lt_apart_lt_flip x y : ~(x < y) -> x ≶ y -> y < x.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
~ (x < y) -> x ≶ y -> y < x
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
~ (x < y) -> x ≶ y -> y < x
  intros nlt neq.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
nlt: ~ (x < y)
neq: x ≶ y
y < x apply apart_iff_total_lt in neq.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
nlt: ~ (x < y)
neq: ((x < y) + (y < x))%type
y < x
  destruct neq.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
nlt: ~ (x < y)
l: x < y
y < x
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
nlt: ~ (x < y)
l: y < x
y < x
  -
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
nlt: ~ (x < y)
l: x < y
y < x destruct nlt;auto.
  -
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
nlt: ~ (x < y)
l: y < x
y < x auto.
  Qed.

  Lemma pseudo_order_cotrans_twice x₁ y₁ x₂ y₂
    : x₁ < y₁ -> merely (x₂ < y₂ |_| x₁ < x₂ |_| y₂ < y₁).
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x₁, y₁, x₂, y₂: A
x₁ < y₁ ->
merely ((x₂ < y₂) + ((x₁ < x₂) + (y₂ < y₁)))
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x₁, y₁, x₂, y₂: A
x₁ < y₁ ->
merely ((x₂ < y₂) + ((x₁ < x₂) + (y₂ < y₁)))
  intros E1.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x₁, y₁, x₂, y₂: A
E1: x₁ < y₁
merely ((x₂ < y₂) + ((x₁ < x₂) + (y₂ < y₁)))
  apply (merely_destruct (cotransitive E1 x₂));intros [?|E2];
  try solve [apply tr;auto].
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x₁, y₁, x₂, y₂: A
E1: x₁ < y₁
E2: x₂ < y₁
merely ((x₂ < y₂) + ((x₁ < x₂) + (y₂ < y₁)))
  apply (merely_destruct (cotransitive E2 y₂));intros [?|?];apply tr;auto.
  Qed.

  Lemma pseudo_order_lt_ext x₁ y₁ x₂ y₂ : x₁ < y₁ ->
    merely (x₂ < y₂ |_| x₁ ≶ x₂ |_| y₂ ≶ y₁).
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x₁, y₁, x₂, y₂: A
x₁ < y₁ ->
merely ((x₂ < y₂) + ((x₁ ≶ x₂) + (y₂ ≶ y₁)))
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x₁, y₁, x₂, y₂: A
x₁ < y₁ ->
merely ((x₂ < y₂) + ((x₁ ≶ x₂) + (y₂ ≶ y₁)))
  intros E.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x₁, y₁, x₂, y₂: A
E: x₁ < y₁
merely ((x₂ < y₂) + ((x₁ ≶ x₂) + (y₂ ≶ y₁)))
  apply (merely_destruct (pseudo_order_cotrans_twice x₁ y₁ x₂ y₂ E));
  intros [?|[?|?]];apply tr;
  auto using pseudo_order_lt_apart.
  Qed.

  #[export] Instance pseudoorder_strictorder : StrictOrder (_ : Lt A).
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
StrictOrder (Alt : Lt A)
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
StrictOrder (Alt : Lt A)
  split.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
is_mere_relation A lt
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
Irreflexive lt
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
Transitive lt
  -
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
is_mere_relation A lt exact _.
  -
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
Irreflexive lt intros x E.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x: A
E: x < x
Empty
    destruct (pseudo_order_antisym x x); auto.
  -
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
Transitive lt intros x y z E1 E2.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
E1: x < y
E2: y < z
x < z
    apply (merely_destruct (cotransitive E1 z));intros [?|?]; trivial.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
E1: x < y
E2: y < z
l: z < y
x < z
    destruct (pseudo_order_antisym y z); auto.
  Qed.

  #[export] Instance nlt_trans : Transitive (complement (<)).
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
Transitive (complement lt)
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
Transitive (complement lt)
  intros x y z.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
complement lt x y ->
complement lt y z -> complement lt x z
  intros E1 E2 E3.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
E1: complement lt x y
E2: complement lt y z
E3: x < z
Empty
  apply (merely_destruct (cotransitive E3 y));
  intros [?|?]; contradiction.
  Qed.

  #[export] Instance nlt_antisymm : AntiSymmetric (complement (<)).
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
AntiSymmetric (complement lt)
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
AntiSymmetric (complement lt)
  intros x y H1 H2.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
H1: complement lt x y
H2: complement lt y x
x = y
  apply tight_apart.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
H1: complement lt x y
H2: complement lt y x
~ (x ≶ y) intros nap.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
H1: complement lt x y
H2: complement lt y x
nap: x ≶ y
Empty apply apart_iff_total_lt in nap.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y: A
H1: complement lt x y
H2: complement lt y x
nap: ((x < y) + (y < x))%type
Empty
  destruct nap;auto.
  Qed.

  Lemma ne_total_lt `{!TrivialApart A} x y : x <> y -> x < y |_| y < x.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
TrivialApart0: TrivialApart A
x, y: A
x <> y -> (x < y) + (y < x)
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
TrivialApart0: TrivialApart A
x, y: A
x <> y -> (x < y) + (y < x)
  intros neq;apply trivial_apart in neq.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
TrivialApart0: TrivialApart A
x, y: A
neq: x ≶ y
((x < y) + (y < x))%type
  apply apart_total_lt.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
TrivialApart0: TrivialApart A
x, y: A
neq: x ≶ y
x ≶ y assumption.
  Qed.

  #[export] Instance lt_trichotomy `{!TrivialApart A} `{DecidablePaths A}
    : Trichotomy (<).
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
Trichotomy lt
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
Trichotomy lt
  intros x y.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
((x < y) + ((x = y) + (y < x)))%type
  destruct (dec (x = y)) as [?|?]; try auto.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
n: x <> y
((x < y) + ((x = y) + (y < x)))%type
  destruct (ne_total_lt x y); auto.
  Qed.
End pseudo_order.

Section full_partial_order.
  Context `{FullPartialOrder A}.

  Local Existing Instance strict_po_apart.

  (* Duplicate of strong_setoids.apart_ne. This is useful because a
    StrongSetoid is not defined as a substructure of a FullPartialOrder *)
  Instance strict_po_apart_ne x y : PropHolds (x ≶ y) -> PropHolds (x <> y).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
PropHolds (x ≶ y) -> PropHolds (x <> y)
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
PropHolds (x ≶ y) -> PropHolds (x <> y)
  intros; exact _.
  Qed.

  #[export] Instance fullpartialorder_strictorder : StrictOrder (<).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
StrictOrder lt
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
StrictOrder lt
  split; try exact _.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
is_mere_relation A lt
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
Irreflexive lt
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
is_mere_relation A lt exact strict_po_mere_lt.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
Irreflexive lt intros x.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x: A
complement lt x x red.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x: A
~ (x < x) intros E;apply lt_iff_le_apart in E.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x: A
E: ((x ≤ x) * (x ≶ x))%type
Empty
    destruct E as [_ ?].
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x: A
snd: x ≶ x
Empty
    apply (irreflexivity (≶) x).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x: A
snd: x ≶ x
x ≶ x
    assumption.
  Qed.

  Lemma lt_le x y : PropHolds (x < y) -> PropHolds (x ≤ y).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
PropHolds (x < y) -> PropHolds (x ≤ y)
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
PropHolds (x < y) -> PropHolds (x ≤ y)
  intro.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
X: PropHolds (x < y)
PropHolds (x ≤ y)
  apply lt_iff_le_apart.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
X: PropHolds (x < y)
x < y
  assumption.
  Qed.

  Lemma not_le_not_lt x y : ~(x ≤ y) -> ~(x < y).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
~ (x ≤ y) -> ~ (x < y)
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
~ (x ≤ y) -> ~ (x < y)
  intros E1 E2.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
E1: ~ (x ≤ y)
E2: x < y
Empty
  apply E1.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
E1: ~ (x ≤ y)
E2: x < y
x ≤ y apply lt_le.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
E1: ~ (x ≤ y)
E2: x < y
PropHolds (x < y) assumption.
  Qed.

  Lemma lt_apart x y : x < y -> x ≶ y.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
x < y -> x ≶ y
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
x < y -> x ≶ y
  intro.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
X: x < y
x ≶ y
  apply lt_iff_le_apart.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
X: x < y
x < y
  assumption.
  Qed.

  Lemma lt_apart_flip x y : x < y -> y ≶ x.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
x < y -> y ≶ x
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
x < y -> y ≶ x
  intro.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
X: x < y
y ≶ x
  apply symmetry, lt_iff_le_apart.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
X: x < y
x < y
  assumption.
  Qed.

  Lemma le_not_lt_flip x y : y ≤ x -> ~(x < y).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
y ≤ x -> ~ (x < y)
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
y ≤ x -> ~ (x < y)
  intros E1 E2;apply lt_iff_le_apart in E2.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
E1: y ≤ x
E2: ((x ≤ y) * (x ≶ y))%type
Empty
  destruct E2 as [E2a E2b].
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
E1: y ≤ x
E2a: x ≤ y
E2b: x ≶ y
Empty
  revert E2b.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
E1: y ≤ x
E2a: x ≤ y
x ≶ y -> Empty apply tight_apart.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
E1: y ≤ x
E2a: x ≤ y
x = y
  apply (antisymmetry (≤));assumption.
  Qed.

  Lemma lt_not_le_flip x y : y < x -> ~(x ≤ y).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
y < x -> ~ (x ≤ y)
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
y < x -> ~ (x ≤ y)
  intros E1 E2.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y: A
E1: y < x
E2: x ≤ y
Empty
  apply (le_not_lt_flip y x);assumption.
  Qed.

  Lemma lt_le_trans x y z : x < y -> y ≤ z -> x < z.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
x < y -> y ≤ z -> x < z
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
x < y -> y ≤ z -> x < z
  intros E1 E2.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E1: x < y
E2: y ≤ z
x < z
  apply lt_iff_le_apart.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E1: x < y
E2: y ≤ z
((x ≤ z) * (x ≶ z))%type apply lt_iff_le_apart in E1.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E1: ((x ≤ y) * (x ≶ y))%type
E2: y ≤ z
((x ≤ z) * (x ≶ z))%type
  destruct E1 as [E1a E1b].
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E1a: x ≤ y
E1b: x ≶ y
E2: y ≤ z
((x ≤ z) * (x ≶ z))%type
  split.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E1a: x ≤ y
E1b: x ≶ y
E2: y ≤ z
x ≤ z
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E1a: x ≤ y
E1b: x ≶ y
E2: y ≤ z
x ≶ z
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E1a: x ≤ y
E1b: x ≶ y
E2: y ≤ z
x ≤ z transitivity y;assumption.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E1a: x ≤ y
E1b: x ≶ y
E2: y ≤ z
x ≶ z apply (merely_destruct (cotransitive E1b z));intros [E3 | E3]; trivial.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E1a: x ≤ y
E1b: x ≶ y
E2: y ≤ z
E3: z ≶ y
x ≶ z
    apply lt_apart.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E1a: x ≤ y
E1b: x ≶ y
E2: y ≤ z
E3: z ≶ y
x < z apply symmetry in E3.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E1a: x ≤ y
E1b: x ≶ y
E2: y ≤ z
E3: y ≶ z
x < z
    transitivity y;apply lt_iff_le_apart; auto.
  Qed.

  Lemma le_lt_trans x y z : x ≤ y -> y < z -> x < z.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
x ≤ y -> y < z -> x < z
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
x ≤ y -> y < z -> x < z
  intros E2 E1.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E2: x ≤ y
E1: y < z
x < z
  apply lt_iff_le_apart.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E2: x ≤ y
E1: y < z
((x ≤ z) * (x ≶ z))%type apply lt_iff_le_apart in E1.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E2: x ≤ y
E1: ((y ≤ z) * (y ≶ z))%type
((x ≤ z) * (x ≶ z))%type
  destruct E1 as [E1a E1b].
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E2: x ≤ y
E1a: y ≤ z
E1b: y ≶ z
((x ≤ z) * (x ≶ z))%type
  split.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E2: x ≤ y
E1a: y ≤ z
E1b: y ≶ z
x ≤ z
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E2: x ≤ y
E1a: y ≤ z
E1b: y ≶ z
x ≶ z
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E2: x ≤ y
E1a: y ≤ z
E1b: y ≶ z
x ≤ z transitivity y;auto.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E2: x ≤ y
E1a: y ≤ z
E1b: y ≶ z
x ≶ z apply (merely_destruct (cotransitive E1b x));intros [E3 | E3]; trivial.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E2: x ≤ y
E1a: y ≤ z
E1b: y ≶ z
E3: y ≶ x
x ≶ z
    apply lt_apart.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E2: x ≤ y
E1a: y ≤ z
E1b: y ≶ z
E3: y ≶ x
x < z apply symmetry in E3.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
x, y, z: A
E2: x ≤ y
E1a: y ≤ z
E1b: y ≶ z
E3: x ≶ y
x < z
    transitivity y; apply lt_iff_le_apart; auto.
  Qed.

  Lemma lt_iff_le_ne `{!TrivialApart A} x y : x < y <-> x ≤ y /\ x <> y.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
x, y: A
x < y <-> (x ≤ y) * (x <> y)
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
x, y: A
x < y <-> (x ≤ y) * (x <> y)
   transitivity (x <= y /\ apart x y).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
x, y: A
x < y <-> (x ≤ y) * (x ≶ y)
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
x, y: A
(x ≤ y) * (x ≶ y) <-> (x ≤ y) * (x <> y)
   -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
x, y: A
x < y <-> (x ≤ y) * (x ≶ y) apply lt_iff_le_apart.
   -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
x, y: A
(x ≤ y) * (x ≶ y) <-> (x ≤ y) * (x <> y) split;intros [E1 E2];split;trivial;apply trivial_apart;trivial.
  Qed.

  Lemma le_equiv_lt `{!TrivialApart A} `{forall x y : A, Decidable (x = y)} x y
    : x ≤ y -> x = y |_| x < y.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x = y)
x, y: A
x ≤ y -> (x = y) + (x < y)
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x = y)
x, y: A
x ≤ y -> (x = y) + (x < y)
  intros.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x = y)
x, y: A
X: x ≤ y
((x = y) + (x < y))%type
  destruct (dec (x = y)); try auto.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x = y)
x, y: A
X: x ≤ y
n: x <> y
((x = y) + (x < y))%type
  right.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x = y)
x, y: A
X: x ≤ y
n: x <> y
x < y
  apply lt_iff_le_ne; auto.
  Qed.

  Instance dec_from_lt_dec `{!TrivialApart A} `{forall x y, Decidable (x ≤ y)}
    : DecidablePaths A.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
DecidablePaths A
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
DecidablePaths A
  intros x y.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
Decidable (x = y)
  destruct (decide_rel (<=) x y) as [E1|E1];
  [destruct (decide_rel (<=) y x) as [E2|E2]|].
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: x ≤ y
E2: y ≤ x
Decidable (x = y)
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: x ≤ y
E2: ~ (y ≤ x)
Decidable (x = y)
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: ~ (x ≤ y)
Decidable (x = y)
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: x ≤ y
E2: y ≤ x
Decidable (x = y) left.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: x ≤ y
E2: y ≤ x
x = y apply (antisymmetry (<=));assumption.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: x ≤ y
E2: ~ (y ≤ x)
Decidable (x = y) right.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: x ≤ y
E2: ~ (y ≤ x)
x <> y intros E3;apply E2.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: x ≤ y
E2: ~ (y ≤ x)
E3: x = y
y ≤ x
    pattern y.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: x ≤ y
E2: ~ (y ≤ x)
E3: x = y
(fun a : A => a ≤ x) y apply (transport _ E3).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: x ≤ y
E2: ~ (y ≤ x)
E3: x = y
x ≤ x
    apply reflexivity.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: ~ (x ≤ y)
Decidable (x = y) right.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: ~ (x ≤ y)
x <> y intros E3;apply E1.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: ~ (x ≤ y)
E3: x = y
x ≤ y
    pattern y; apply (transport _ E3).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
E1: ~ (x ≤ y)
E3: x = y
x ≤ x
    apply reflexivity.
  Defined.

  Definition lt_dec_slow `{!TrivialApart A} `{forall x y, Decidable (x ≤ y)} :
    forall x y, Decidable (x < y).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
forall x y : A, Decidable (x < y)
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
forall x y : A, Decidable (x < y)
  intros x y.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
Decidable (x < y)
  destruct (dec (x ≤ y));
  [destruct (dec (x = y))|].
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
l: x ≤ y
p: x = y
Decidable (x < y)
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
l: x ≤ y
n: x <> y
Decidable (x < y)
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
n: ~ (x ≤ y)
Decidable (x < y)
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
l: x ≤ y
p: x = y
Decidable (x < y) right.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
l: x ≤ y
p: x = y
~ (x < y) apply eq_not_lt.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
l: x ≤ y
p: x = y
x = y assumption.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
l: x ≤ y
n: x <> y
Decidable (x < y) left.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
l: x ≤ y
n: x <> y
x < y apply lt_iff_le_ne.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
l: x ≤ y
n: x <> y
((x ≤ y) * (x <> y))%type auto.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
n: ~ (x ≤ y)
Decidable (x < y) right.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
n: ~ (x ≤ y)
~ (x < y) apply not_le_not_lt.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
n: ~ (x ≤ y)
~ (x ≤ y) assumption.
  Defined.
End full_partial_order.

(* Due to bug #2528 *)
#[export]
Hint Extern 5 (PropHolds (_ <> _)) =>
  eapply @strict_po_apart_ne :  typeclass_instances.
#[export]
Hint Extern 10 (PropHolds (_ ≤ _)) =>
  eapply @lt_le : typeclass_instances.
#[export]
Hint Extern 20 (Decidable (_ < _)) =>
  eapply @lt_dec_slow : typeclass_instances.

Section full_pseudo_order.
  Context `{FullPseudoOrder A}.

  Local Existing Instance pseudo_order_apart.

  Lemma not_lt_le_flip x y : ~(y < x) -> x ≤ y.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
~ (y < x) -> x ≤ y
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
~ (y < x) -> x ≤ y
  intros.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
X: ~ (y < x)
x ≤ y
  apply le_iff_not_lt_flip.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
X: ~ (y < x)
~ (y < x)
  assumption.
  Qed.

  Instance fullpseudo_partial : PartialOrder (≤) | 10.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
PartialOrder le
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
PartialOrder le
  repeat split.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
IsHSet A
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
is_mere_relation A le
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
Reflexive le
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
Transitive le
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
AntiSymmetric le
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
IsHSet A exact _.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
is_mere_relation A le exact _.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
Reflexive le intros x.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x: A
x ≤ x apply not_lt_le_flip, (irreflexivity (<)).
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
Transitive le intros x y z E1 E2.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y, z: A
E1: x ≤ y
E2: y ≤ z
x ≤ z
    apply le_iff_not_lt_flip;
    apply le_iff_not_lt_flip in E1;
    apply le_iff_not_lt_flip in E2.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y, z: A
E1: ~ (y < x)
E2: ~ (z < y)
~ (z < x)
    change (complement (<) z x).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y, z: A
E1: ~ (y < x)
E2: ~ (z < y)
complement lt z x
    transitivity y;assumption.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
AntiSymmetric le intros x y E1 E2.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
E1: x ≤ y
E2: y ≤ x
x = y
    apply le_iff_not_lt_flip in E1;
    apply le_iff_not_lt_flip in E2.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
E1: ~ (y < x)
E2: ~ (x < y)
x = y
    apply (antisymmetry (complement (<)));assumption.
  Qed.

  Lemma fullpseudo_fullpartial' : FullPartialOrder Ale Alt.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
FullPartialOrder Ale Alt
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
FullPartialOrder Ale Alt
  split; try exact _.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
forall x y : A, x < y <-> (x ≤ y) * (x ≶ y)
  intros x y.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
x < y <-> (x ≤ y) * (x ≶ y)
  split.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
x < y -> (x ≤ y) * (x ≶ y)
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
(x ≤ y) * (x ≶ y) -> x < y
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
x < y -> (x ≤ y) * (x ≶ y) intros E.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
E: x < y
((x ≤ y) * (x ≶ y))%type split.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
E: x < y
x ≤ y
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
E: x < y
x ≶ y
    +
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
E: x < y
x ≤ y apply not_lt_le_flip.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
E: x < y
~ (y < x) apply lt_flip;assumption.
    +
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
E: x < y
x ≶ y apply pseudo_order_lt_apart.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
E: x < y
x < y assumption.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
(x ≤ y) * (x ≶ y) -> x < y intros [? E].
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
fst: x ≤ y
E: x ≶ y
x < y apply not_lt_apart_lt_flip;[|symmetry;trivial].
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
fst: x ≤ y
E: x ≶ y
~ (y < x)
    apply le_iff_not_lt_flip.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
fst: x ≤ y
E: x ≶ y
x ≤ y trivial.
  Qed.

  #[export] Instance fullpseudo_fullpartial@{i} : FullPartialOrder Ale Alt
    := ltac:(first [exact fullpseudo_fullpartial'@{i i Set Set Set}|
                    exact fullpseudo_fullpartial'@{i i}]).

  #[export] Instance le_stable : forall x y, Stable (x ≤ y).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
forall x y : A, Stable (x ≤ y)
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
forall x y : A, Stable (x ≤ y)
  intros x y.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
Stable (x ≤ y) unfold Stable.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
~~ (x ≤ y) -> x ≤ y
  intros dn.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
dn: ~~ (x ≤ y)
x ≤ y apply le_iff_not_lt_flip.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
dn: ~~ (x ≤ y)
~ (y < x)
  intros E.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
dn: ~~ (x ≤ y)
E: y < x
Empty apply dn.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
x, y: A
dn: ~~ (x ≤ y)
E: y < x
~ (x ≤ y)
  intros E';apply le_iff_not_lt_flip in E';auto.
  Qed.

  Lemma le_or_lt `{!TrivialApart A} `{DecidablePaths A} x y : x ≤ y |_| y < x.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
((x ≤ y) + (y < x))%type
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
((x ≤ y) + (y < x))%type
  destruct (trichotomy (<) x y) as [|[|]]; try auto.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
l: x < y
((x ≤ y) + (y < x))%type
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
p: x = y
((x ≤ y) + (y < x))%type
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
l: x < y
((x ≤ y) + (y < x))%type left.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
l: x < y
x ≤ y apply lt_le;trivial.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
p: x = y
((x ≤ y) + (y < x))%type left.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
p: x = y
x ≤ y apply eq_le;trivial.
  Qed.

  #[export] Instance le_total `{!TrivialApart A} `{DecidablePaths A}
    : TotalOrder (≤).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
TotalOrder le
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
TotalOrder le
  split; try exact _.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
TotalRelation le
  intros x y.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
((x ≤ y) + (y ≤ x))%type
  destruct (le_or_lt x y); auto.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
l: y < x
((x ≤ y) + (y ≤ x))%type
  right.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
l: y < x
y ≤ x apply lt_le.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
l: y < x
PropHolds (y < x)
  trivial.
  Qed.

  Lemma not_le_lt_flip `{!TrivialApart A} `{DecidablePaths A} x y
    : ~(y ≤ x) -> x < y.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
~ (y ≤ x) -> x < y
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
~ (y ≤ x) -> x < y
  intros.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
X: ~ (y ≤ x)
x < y
  destruct (le_or_lt y x); auto.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: DecidablePaths A
x, y: A
X: ~ (y ≤ x)
l: y ≤ x
x < y
  contradiction.
  Qed.

  Existing Instance dec_from_lt_dec.

  Definition lt_dec `{!TrivialApart A} `{forall x y, Decidable (x ≤ y)}
    : forall x y, Decidable (x < y).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
forall x y : A, Decidable (x < y)
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
forall x y : A, Decidable (x < y)
  intros.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
Decidable (x < y)
  destruct (decide_rel (<=) y x).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
l: y ≤ x
Decidable (x < y)
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
n: ~ (y ≤ x)
Decidable (x < y)
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
l: y ≤ x
Decidable (x < y) right;apply le_not_lt_flip;assumption.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
TrivialApart0: TrivialApart A
H0: forall x y : A, Decidable (x ≤ y)
x, y: A
n: ~ (y ≤ x)
Decidable (x < y) left; apply not_le_lt_flip;assumption.
  Defined.
End full_pseudo_order.

#[export]
Hint Extern 8 (Decidable (_ < _)) => eapply @lt_dec : typeclass_instances.
(*
The following instances would be tempting, but turn out to be a bad idea.

#[export]
Hint Extern 10 (PropHolds (_ <> _)) => eapply @le_ne : typeclass_instances.
#[export]
Hint Extern 10 (PropHolds (_ <> _)) => eapply @le_ne_flip : typeclass_instances.

It will then loop like:

semirings.lt_0_1 -> lt_ne_flip -> ...
*)

Section dec_strict_setoid_order.
  Context `{StrictOrder A} `{Apart A} `{!TrivialApart A} `{DecidablePaths A}.

  Instance: IsApart A := dec_strong_setoid.

  Context `{!Trichotomy (<)}.

  Instance dec_strict_pseudo_order: PseudoOrder (<).
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
PseudoOrder lt
  Proof.
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
PseudoOrder lt
  split; try exact _.
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
forall x y : A, ~ (x < y < x)
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
CoTransitive lt
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
forall x y : A, x ≶ y <-> (x < y) + (y < x)
  -
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
forall x y : A, ~ (x < y < x) intros x y [??].
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
fst: x < y
snd: y < x
Empty
    destruct (lt_antisym x y); auto.
  -
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
CoTransitive lt intros x y Exy z.
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
Exy: x < y
z: A
hor (x < z) (z < y)
    destruct (trichotomy (<) x z) as [? | [Exz | Exz]];apply tr; try auto.
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
Exy: x < y
z: A
Exz: x = z
((x < z) + (z < y))%type
    right.
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
Exy: x < y
z: A
Exz: x = z
z < y rewrite <-Exz.
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
Exy: x < y
z: A
Exz: x = z
x < y assumption.
  -
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
forall x y : A, x ≶ y <-> (x < y) + (y < x) intros x y.
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
x ≶ y <-> (x < y) + (y < x) transitivity (x <> y);[split;apply trivial_apart|].
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
x <> y <-> (x < y) + (y < x)
    split.
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
x <> y -> (x < y) + (y < x)
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
(x < y) + (y < x) -> x <> y
    +
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
x <> y -> (x < y) + (y < x) destruct (trichotomy (<) x y) as [?|[?|?]]; auto.
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
p: x = y
x <> y -> (x < y) + (y < x)
      intros E;contradiction E.
    +
A: Type
Alt: Lt A
H: StrictOrder Alt
H0: Apart A
TrivialApart0: TrivialApart A
H1: DecidablePaths A
Trichotomy0: Trichotomy lt
x, y: A
(x < y) + (y < x) -> x <> y intros [?|?];[apply lt_ne|apply lt_ne_flip];trivial.
  Qed.
End dec_strict_setoid_order.

Section dec_partial_order.
  Context `{PartialOrder A} `{DecidablePaths A}.

  Definition dec_lt: Lt A := fun x y => x ≤ y /\ x <> y.

  Context `{Alt : Lt A} `{is_mere_relation A lt}
    (lt_correct : forall x y, x < y <-> x ≤ y /\ x <> y).

  Instance dec_order: StrictOrder (<).
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
StrictOrder lt
  Proof.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
StrictOrder lt
  split.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
is_mere_relation A lt
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
Irreflexive lt
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
Transitive lt
  -
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
is_mere_relation A lt exact _.
  -
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
Irreflexive lt intros x E.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x: A
E: x < x
Empty apply lt_correct in E.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x: A
E: ((x ≤ x) * (x <> x))%type
Empty destruct E as [_ []];trivial.
  -
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
Transitive lt intros x y z E1 E2.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x, y, z: A
E1: x < y
E2: y < z
x < z
    apply lt_correct;
    apply lt_correct in E1;
    apply lt_correct in E2.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x, y, z: A
E1: ((x ≤ y) * (x <> y))%type
E2: ((y ≤ z) * (y <> z))%type
((x ≤ z) * (x <> z))%type
    destruct E1 as [E1a E1b],E2 as [E2a E2b].
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x, y, z: A
E1a: x ≤ y
E1b: x <> y
E2a: y ≤ z
E2b: y <> z
((x ≤ z) * (x <> z))%type
    split.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x, y, z: A
E1a: x ≤ y
E1b: x <> y
E2a: y ≤ z
E2b: y <> z
x ≤ z
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x, y, z: A
E1a: x ≤ y
E1b: x <> y
E2a: y ≤ z
E2b: y <> z
x <> z
    +
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x, y, z: A
E1a: x ≤ y
E1b: x <> y
E2a: y ≤ z
E2b: y <> z
x ≤ z transitivity y;trivial.
    +
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x, y, z: A
E1a: x ≤ y
E1b: x <> y
E2a: y ≤ z
E2b: y <> z
x <> z intros E3.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x, y, z: A
E1a: x ≤ y
E1b: x <> y
E2a: y ≤ z
E2b: y <> z
E3: x = z
Empty destruct E2b.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x, y, z: A
E1a: x ≤ y
E1b: x <> y
E2a: y ≤ z
E3: x = z
y = z
      apply (antisymmetry (≤)); trivial.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x, y, z: A
E1a: x ≤ y
E1b: x <> y
E2a: y ≤ z
E3: x = z
z ≤ y
      rewrite <-E3.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
x, y, z: A
E1a: x ≤ y
E1b: x <> y
E2a: y ≤ z
E3: x = z
x ≤ y assumption.
  Qed.

  Context `{Apart A} `{!TrivialApart A}.

  Instance: IsApart A := dec_strong_setoid.

  Instance dec_full_partial_order: FullPartialOrder (≤) (<).
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
FullPartialOrder le lt
  Proof.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
FullPartialOrder le lt
  split;try exact _.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
forall x y : A, x < y <-> (x ≤ y) * (x ≶ y)
  intros.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
x, y: A
x < y <-> (x ≤ y) * (x ≶ y) transitivity (x <= y /\ x <> y);[|
  split;intros [? ?];split;trivial;apply trivial_apart;trivial].
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
x, y: A
x < y <-> (x ≤ y) * (x <> y)
  apply lt_correct.
  Qed.

  Context `{!TotalRelation (≤)}.

  Instance: Trichotomy (<).
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
Trichotomy lt
  Proof.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
Trichotomy lt
  intros x y.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
((x < y) + ((x = y) + (y < x)))%type
  destruct (dec (x = y)); try auto.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
n: x <> y
((x < y) + ((x = y) + (y < x)))%type
  destruct (total (≤) x y);[left|right;right];
  apply lt_correct;auto.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
n: x <> y
l: y ≤ x
((y ≤ x) * (y <> x))%type
  split;auto.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
n: x <> y
l: y ≤ x
y <> x
  intro E;apply symmetry in E;auto.
  Qed.

  Instance dec_pseudo_order: PseudoOrder (<) := dec_strict_pseudo_order.

  Instance dec_full_pseudo_order: FullPseudoOrder (≤) (<).
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
FullPseudoOrder le lt
  Proof.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
FullPseudoOrder le lt
  split; try exact _.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
forall x y : A, x ≤ y <-> ~ (y < x)
  intros x y.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
x ≤ y <-> ~ (y < x)
  split.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
x ≤ y -> ~ (y < x)
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
~ (y < x) -> x ≤ y
  -
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
x ≤ y -> ~ (y < x) intros ? E.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
X: x ≤ y
E: y < x
Empty apply lt_correct in E;destruct E as [? []].
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
X: x ≤ y
fst: y ≤ x
y = x
    apply (antisymmetry (≤));assumption.
  -
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
~ (y < x) -> x ≤ y intros E1.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
E1: ~ (y < x)
x ≤ y
    destruct (total (≤) x y); trivial.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
E1: ~ (y < x)
l: y ≤ x
x ≤ y
    destruct (dec (x = y)) as [E2|E2].
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
E1: ~ (y < x)
l: y ≤ x
E2: x = y
x ≤ y
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
E1: ~ (y < x)
l: y ≤ x
E2: x <> y
x ≤ y
    +
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
E1: ~ (y < x)
l: y ≤ x
E2: x = y
x ≤ y rewrite E2.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
E1: ~ (y < x)
l: y ≤ x
E2: x = y
y ≤ y apply reflexivity.
    +
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
E1: ~ (y < x)
l: y ≤ x
E2: x <> y
x ≤ y destruct E1.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
l: y ≤ x
E2: x <> y
y < x apply lt_correct;split;auto.
A: Type
Ale: Le A
H: PartialOrder Ale
H0: DecidablePaths A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
lt_correct: forall x y : A,
x < y <-> (x ≤ y) * (x <> y)
H1: Apart A
TrivialApart0: TrivialApart A
TotalRelation0: TotalRelation le
x, y: A
l: y ≤ x
E2: x <> y
y <> x
      apply symmetric_neq;assumption.
  Qed.
End dec_partial_order.

Lemma lt_eq_trans `{Lt A} : forall x y z, x < y -> y = z -> x < z.
A: Type
H: Lt A
forall x y z : A, x < y -> y = z -> x < z
Proof.
A: Type
H: Lt A
forall x y z : A, x < y -> y = z -> x < z
intros ???? [];trivial.
Qed.

Section pseudo.
  Context {A : Type}.
  Context `{PseudoOrder A}.

  Lemma nlt_lt_trans {x y z : A} : ~ (y < x) -> y < z -> x < z.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
~ (y < x) -> y < z -> x < z
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
~ (y < x) -> y < z -> x < z
    intros nltyx ltyz.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
nltyx: ~ (y < x)
ltyz: y < z
x < z
    assert (disj := cotransitive ltyz x).
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
nltyx: ~ (y < x)
ltyz: y < z
disj: hor (y < x) (x < z)
x < z
    strip_truncations.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
nltyx: ~ (y < x)
ltyz: y < z
disj: ((y < x) + (x < z))%type
x < z
    destruct disj as [ltyx|ltxz].
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
nltyx: ~ (y < x)
ltyz: y < z
ltyx: y < x
x < z
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
nltyx: ~ (y < x)
ltyz: y < z
ltxz: x < z
x < z
    -
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
nltyx: ~ (y < x)
ltyz: y < z
ltyx: y < x
x < z destruct (nltyx ltyx).
    -
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
nltyx: ~ (y < x)
ltyz: y < z
ltxz: x < z
x < z exact ltxz.
  Qed.

  Lemma lt_nlt_trans {x y z : A} : x < y -> ~ (z < y) -> x < z.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
x < y -> ~ (z < y) -> x < z
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
x < y -> ~ (z < y) -> x < z
    intros ltxy nltzy.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: x < y
nltzy: ~ (z < y)
x < z
    assert (disj := cotransitive ltxy z).
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: x < y
nltzy: ~ (z < y)
disj: hor (x < z) (z < y)
x < z
    strip_truncations.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: x < y
nltzy: ~ (z < y)
disj: ((x < z) + (z < y))%type
x < z
    destruct disj as [ltxz|ltzy].
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: x < y
nltzy: ~ (z < y)
ltxz: x < z
x < z
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: x < y
nltzy: ~ (z < y)
ltzy: z < y
x < z
    -
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: x < y
nltzy: ~ (z < y)
ltxz: x < z
x < z exact ltxz.
    -
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: x < y
nltzy: ~ (z < y)
ltzy: z < y
x < z destruct (nltzy ltzy).
  Qed.

  Lemma lt_transitive : Transitive (_ : Lt A).
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
Transitive (Alt : Lt A)
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
Transitive (Alt : Lt A)
    intros x y z ltxy ltyz.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: Alt x y
ltyz: Alt y z
Alt x z
    assert (ltxyz := cotransitive ltxy z).
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: Alt x y
ltyz: Alt y z
ltxyz: hor (Alt x z) (Alt z y)
Alt x z
    strip_truncations.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: Alt x y
ltyz: Alt y z
ltxyz: (Alt x z + Alt z y)%type
Alt x z
    destruct ltxyz as [ltxz|ltzy].
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: Alt x y
ltyz: Alt y z
ltxz: Alt x z
Alt x z
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: Alt x y
ltyz: Alt y z
ltzy: Alt z y
Alt x z
    -
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: Alt x y
ltyz: Alt y z
ltxz: Alt x z
Alt x z assumption.
    -
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
x, y, z: A
ltxy: Alt x y
ltyz: Alt y z
ltzy: Alt z y
Alt x z destruct (pseudo_order_antisym y z (ltyz , ltzy)).
  Qed.

  #[export] Existing Instance lt_transitive.

End pseudo.