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

Generalizable Variables A B C R S f g z.

(* If a function between strict partial orders is order preserving (back), we can
  derive that it is strictly order preserving (back) *)
Section strictly_order_preserving.
  Context `{FullPartialOrder A} `{FullPartialOrder B}.

  #[export] Instance strictly_order_preserving_inj  `{!OrderPreserving (f : A -> B)}
    `{!IsStrongInjective f} :
    StrictlyOrderPreserving f | 20.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsStrongInjective0: IsStrongInjective f
StrictlyOrderPreserving f
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsStrongInjective0: IsStrongInjective f
StrictlyOrderPreserving f
  intros x y E.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsStrongInjective0: IsStrongInjective f
x, y: A
E: x < y
f x < f y
  apply lt_iff_le_apart in E.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsStrongInjective0: IsStrongInjective f
x, y: A
E: ((x ≤ y) * (x ≶ y))%type
f x < f y apply lt_iff_le_apart.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsStrongInjective0: IsStrongInjective f
x, y: A
E: ((x ≤ y) * (x ≶ y))%type
((f x ≤ f y) * (f x ≶ f y))%type
  destruct E as [E1 E2].
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsStrongInjective0: IsStrongInjective f
x, y: A
E1: x ≤ y
E2: x ≶ y
((f x ≤ f y) * (f x ≶ f y))%type split.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsStrongInjective0: IsStrongInjective f
x, y: A
E1: x ≤ y
E2: x ≶ y
f x ≤ f y
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsStrongInjective0: IsStrongInjective f
x, y: A
E1: x ≤ y
E2: x ≶ y
f x ≶ f y
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsStrongInjective0: IsStrongInjective f
x, y: A
E1: x ≤ y
E2: x ≶ y
f x ≤ f y apply (order_preserving f);trivial.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsStrongInjective0: IsStrongInjective f
x, y: A
E1: x ≤ y
E2: x ≶ y
f x ≶ f y apply (strong_injective f);trivial.
  Qed.

  #[export] Instance strictly_order_reflecting_mor `{!OrderReflecting (f : A -> B)}
    `{!StrongExtensionality f} :
    StrictlyOrderReflecting f | 20.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrongExtensionality0: StrongExtensionality f
StrictlyOrderReflecting f
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrongExtensionality0: StrongExtensionality f
StrictlyOrderReflecting f
  intros x y E.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrongExtensionality0: StrongExtensionality f
x, y: A
E: f x < f y
x < y
  apply lt_iff_le_apart in E.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrongExtensionality0: StrongExtensionality f
x, y: A
E: ((f x ≤ f y) * (f x ≶ f y))%type
x < y apply lt_iff_le_apart.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrongExtensionality0: StrongExtensionality f
x, y: A
E: ((f x ≤ f y) * (f x ≶ f y))%type
((x ≤ y) * (x ≶ y))%type
  destruct E as [E1 E2].
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrongExtensionality0: StrongExtensionality f
x, y: A
E1: f x ≤ f y
E2: f x ≶ f y
((x ≤ y) * (x ≶ y))%type split.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrongExtensionality0: StrongExtensionality f
x, y: A
E1: f x ≤ f y
E2: f x ≶ f y
x ≤ y
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrongExtensionality0: StrongExtensionality f
x, y: A
E1: f x ≤ f y
E2: f x ≶ f y
x ≶ y
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrongExtensionality0: StrongExtensionality f
x, y: A
E1: f x ≤ f y
E2: f x ≶ f y
x ≤ y apply (order_reflecting f);trivial.
  -
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrongExtensionality0: StrongExtensionality f
x, y: A
E1: f x ≤ f y
E2: f x ≶ f y
x ≶ y apply (strong_extensionality f);trivial.
  Qed.
End strictly_order_preserving.

(* For structures with a trivial apartness relation
   we have a stronger result of the above *)
Section strictly_order_preserving_dec.
  Context `{FullPartialOrder A} `{!TrivialApart A}
          `{FullPartialOrder B} `{!TrivialApart B}.

  Local Existing Instance strict_po_apart.

  #[export] Instance dec_strictly_order_preserving_inj
    `{!OrderPreserving (f : A -> B)}
    `{!IsInjective f} :
    StrictlyOrderPreserving f | 19.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
TrivialApart1: TrivialApart B
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsInjective0: IsInjective f
StrictlyOrderPreserving f
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
TrivialApart1: TrivialApart B
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsInjective0: IsInjective f
StrictlyOrderPreserving f
  pose proof (dec_strong_injective f).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
TrivialApart1: TrivialApart B
f: A -> B
OrderPreserving0: OrderPreserving (f : A -> B)
IsInjective0: IsInjective f
X: IsStrongInjective f
StrictlyOrderPreserving f
  exact _.
  Qed.

  #[export] Instance dec_strictly_order_reflecting_mor
    `{!OrderReflecting (f : A -> B)}
    : StrictlyOrderReflecting f | 19.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
TrivialApart1: TrivialApart B
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrictlyOrderReflecting f
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
TrivialApart1: TrivialApart B
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
StrictlyOrderReflecting f
  pose proof (dec_strong_morphism f).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPartialOrder Ale Alt
TrivialApart0: TrivialApart A
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPartialOrder Ale0 Alt0
TrivialApart1: TrivialApart B
f: A -> B
OrderReflecting0: OrderReflecting (f : A -> B)
X: StrongExtensionality f
StrictlyOrderReflecting f exact _.
  Qed.
End strictly_order_preserving_dec.

Section pseudo_injective.
  Context `{PseudoOrder A} `{PseudoOrder B}.

  Local Existing Instance pseudo_order_apart.

  Instance pseudo_order_embedding_ext `{!StrictOrderEmbedding (f : A -> B)} :
    StrongExtensionality f.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
B: Type
Aap0: Apart B
Alt0: Lt B
H0: PseudoOrder Alt0
f: A -> B
StrictOrderEmbedding0: StrictOrderEmbedding
  (f : A -> B)
StrongExtensionality f
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
B: Type
Aap0: Apart B
Alt0: Lt B
H0: PseudoOrder Alt0
f: A -> B
StrictOrderEmbedding0: StrictOrderEmbedding
  (f : A -> B)
StrongExtensionality f
  intros x y E.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
B: Type
Aap0: Apart B
Alt0: Lt B
H0: PseudoOrder Alt0
f: A -> B
StrictOrderEmbedding0: StrictOrderEmbedding
  (f : A -> B)
x, y: A
E: f x ≶ f y
x ≶ y
  apply apart_iff_total_lt;apply apart_iff_total_lt in E.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
B: Type
Aap0: Apart B
Alt0: Lt B
H0: PseudoOrder Alt0
f: A -> B
StrictOrderEmbedding0: StrictOrderEmbedding
  (f : A -> B)
x, y: A
E: ((f x < f y) + (f y < f x))%type
((x < y) + (y < x))%type
  destruct E; [left | right]; apply (strictly_order_reflecting f);trivial.
  Qed.

  Lemma pseudo_order_embedding_inj `{!StrictOrderEmbedding (f : A -> B)} :
    IsStrongInjective f.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
B: Type
Aap0: Apart B
Alt0: Lt B
H0: PseudoOrder Alt0
f: A -> B
StrictOrderEmbedding0: StrictOrderEmbedding
  (f : A -> B)
IsStrongInjective f
  Proof.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
B: Type
Aap0: Apart B
Alt0: Lt B
H0: PseudoOrder Alt0
f: A -> B
StrictOrderEmbedding0: StrictOrderEmbedding
  (f : A -> B)
IsStrongInjective f
  split;try exact _.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
B: Type
Aap0: Apart B
Alt0: Lt B
H0: PseudoOrder Alt0
f: A -> B
StrictOrderEmbedding0: StrictOrderEmbedding
  (f : A -> B)
forall x y : A, x ≶ y -> f x ≶ f y
  intros x y E.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
B: Type
Aap0: Apart B
Alt0: Lt B
H0: PseudoOrder Alt0
f: A -> B
StrictOrderEmbedding0: StrictOrderEmbedding
  (f : A -> B)
x, y: A
E: x ≶ y
f x ≶ f y
  apply apart_iff_total_lt;apply apart_iff_total_lt in E.
A: Type
Aap: Apart A
Alt: Lt A
H: PseudoOrder Alt
B: Type
Aap0: Apart B
Alt0: Lt B
H0: PseudoOrder Alt0
f: A -> B
StrictOrderEmbedding0: StrictOrderEmbedding
  (f : A -> B)
x, y: A
E: ((x < y) + (y < x))%type
((f x < f y) + (f y < f x))%type
  destruct E; [left | right]; apply (strictly_order_preserving f);trivial.
  Qed.
End pseudo_injective.

(* If a function between pseudo partial orders is strictly order preserving (back),
   we can derive that it is order preserving (back) *)
Section full_pseudo_strictly_preserving.
  Context `{FullPseudoOrder A} `{FullPseudoOrder B}.

  Local Existing Instance pseudo_order_apart.

  Lemma full_pseudo_order_preserving `{!StrictlyOrderReflecting (f : A -> B)}
    : OrderPreserving f.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (f : A -> B)
OrderPreserving f
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (f : A -> B)
OrderPreserving f
  intros x y E1.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (f : A -> B)
x, y: A
E1: x ≤ y
f x ≤ f y
  apply le_iff_not_lt_flip;apply le_iff_not_lt_flip in E1.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (f : A -> B)
x, y: A
E1: ~ (y < x)
~ (f y < f x)
  intros E2.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (f : A -> B)
x, y: A
E1: ~ (y < x)
E2: f y < f x
Empty apply E1.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (f : A -> B)
x, y: A
E1: ~ (y < x)
E2: f y < f x
y < x
  apply (strictly_order_reflecting f).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (f : A -> B)
x, y: A
E1: ~ (y < x)
E2: f y < f x
f y < f x
  trivial.
  Qed.

  Lemma full_pseudo_order_reflecting `{!StrictlyOrderPreserving (f : A -> B)}
    : OrderReflecting f.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderPreserving0: StrictlyOrderPreserving
  (f : A -> B)
OrderReflecting f
  Proof.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderPreserving0: StrictlyOrderPreserving
  (f : A -> B)
OrderReflecting f
  intros x y E1.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderPreserving0: StrictlyOrderPreserving
  (f : A -> B)
x, y: A
E1: f x ≤ f y
x ≤ y
  apply le_iff_not_lt_flip;apply le_iff_not_lt_flip in E1.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderPreserving0: StrictlyOrderPreserving
  (f : A -> B)
x, y: A
E1: ~ (f y < f x)
~ (y < x)
  intros E2.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderPreserving0: StrictlyOrderPreserving
  (f : A -> B)
x, y: A
E1: ~ (f y < f x)
E2: y < x
Empty apply E1.
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderPreserving0: StrictlyOrderPreserving
  (f : A -> B)
x, y: A
E1: ~ (f y < f x)
E2: y < x
f y < f x
  apply (strictly_order_preserving f).
A: Type
Aap: Apart A
Ale: Le A
Alt: Lt A
H: FullPseudoOrder Ale Alt
B: Type
Aap0: Apart B
Ale0: Le B
Alt0: Lt B
H0: FullPseudoOrder Ale0 Alt0
f: A -> B
StrictlyOrderPreserving0: StrictlyOrderPreserving
  (f : A -> B)
x, y: A
E1: ~ (f y < f x)
E2: y < x
y < x
  trivial.
  Qed.
End full_pseudo_strictly_preserving.

(* Some helper lemmas to easily transform order preserving instances. *)
Section order_preserving_ops.
  Context `{Le R}.

  Lemma order_preserving_flip {op} `{!Commutative op} `{!OrderPreserving (op z)}
    : OrderPreserving (fun y => op y z).
R: Type
H: Le R
op: R -> R -> R
Commutative0: Commutative op
z: R
OrderPreserving0: OrderPreserving (op z)
OrderPreserving (fun y : R => op y z)
  Proof.
R: Type
H: Le R
op: R -> R -> R
Commutative0: Commutative op
z: R
OrderPreserving0: OrderPreserving (op z)
OrderPreserving (fun y : R => op y z)
  intros x y E.
R: Type
H: Le R
op: R -> R -> R
Commutative0: Commutative op
z: R
OrderPreserving0: OrderPreserving (op z)
x, y: R
E: x ≤ y
op x z ≤ op y z
  rewrite 2!(commutativity _ z).
R: Type
H: Le R
op: R -> R -> R
Commutative0: Commutative op
z: R
OrderPreserving0: OrderPreserving (op z)
x, y: R
E: x ≤ y
op z x ≤ op z y
  apply order_preserving;trivial.
  Qed.

  Lemma order_reflecting_flip {op} `{!Commutative op}
    `{!OrderReflecting (op z) }
    : OrderReflecting (fun y => op y z).
R: Type
H: Le R
op: R -> R -> R
Commutative0: Commutative op
z: R
OrderReflecting0: OrderReflecting (op z)
OrderReflecting (fun y : R => op y z)
  Proof.
R: Type
H: Le R
op: R -> R -> R
Commutative0: Commutative op
z: R
OrderReflecting0: OrderReflecting (op z)
OrderReflecting (fun y : R => op y z)
  intros x y E.
R: Type
H: Le R
op: R -> R -> R
Commutative0: Commutative op
z: R
OrderReflecting0: OrderReflecting (op z)
x, y: R
E: op x z ≤ op y z
x ≤ y
  apply (order_reflecting (op z)).
R: Type
H: Le R
op: R -> R -> R
Commutative0: Commutative op
z: R
OrderReflecting0: OrderReflecting (op z)
x, y: R
E: op x z ≤ op y z
op z x ≤ op z y
  rewrite 2!(commutativity (f:=op) z).
R: Type
H: Le R
op: R -> R -> R
Commutative0: Commutative op
z: R
OrderReflecting0: OrderReflecting (op z)
x, y: R
E: op x z ≤ op y z
op x z ≤ op y z
  trivial.
  Qed.

  Lemma order_preserving_nonneg (op : R -> R -> R) `{!Zero R}
    `{forall z, PropHolds (0 ≤ z) -> OrderPreserving (op z)} z
    : 0 ≤ z -> forall x y, x ≤ y -> op z x ≤ op z y.
R: Type
H: Le R
op: R -> R -> R
Zero0: Zero R
H0: forall z : R,
PropHolds (0 ≤ z) -> OrderPreserving (op z)
z: R
0 ≤ z -> forall x y : R, x ≤ y -> op z x ≤ op z y
  Proof.
R: Type
H: Le R
op: R -> R -> R
Zero0: Zero R
H0: forall z : R,
PropHolds (0 ≤ z) -> OrderPreserving (op z)
z: R
0 ≤ z -> forall x y : R, x ≤ y -> op z x ≤ op z y
  auto.
  Qed.

  Lemma order_preserving_flip_nonneg (op : R -> R -> R) `{!Zero R}
    {E:forall z, PropHolds (0 ≤ z) -> OrderPreserving (fun y => op y z)} z
    : 0 ≤ z -> forall x y, x ≤ y -> op x z ≤ op y z.
R: Type
H: Le R
op: R -> R -> R
Zero0: Zero R
E: forall z : R,
PropHolds (0 ≤ z) ->
OrderPreserving (fun y : R => op y z)
z: R
0 ≤ z -> forall x y : R, x ≤ y -> op x z ≤ op y z
  Proof.
R: Type
H: Le R
op: R -> R -> R
Zero0: Zero R
E: forall z : R,
PropHolds (0 ≤ z) ->
OrderPreserving (fun y : R => op y z)
z: R
0 ≤ z -> forall x y : R, x ≤ y -> op x z ≤ op y z
  apply E.
  Qed.

  Context `{Lt R}.

  Lemma order_reflecting_pos (op : R -> R -> R) `{!Zero R}
    {E:forall z, PropHolds (0 < z) -> OrderReflecting (op z)} z
    : 0 < z -> forall x y, op z x ≤ op z y -> x ≤ y.
R: Type
H: Le R
H0: Lt R
op: R -> R -> R
Zero0: Zero R
E: forall z : R,
PropHolds (0 < z) -> OrderReflecting (op z)
z: R
0 < z -> forall x y : R, op z x ≤ op z y -> x ≤ y
  Proof.
R: Type
H: Le R
H0: Lt R
op: R -> R -> R
Zero0: Zero R
E: forall z : R,
PropHolds (0 < z) -> OrderReflecting (op z)
z: R
0 < z -> forall x y : R, op z x ≤ op z y -> x ≤ y
  apply E.
  Qed.

  Lemma order_reflecting_flip_pos (op : R -> R -> R) `{!Zero R}
    {E:forall z, PropHolds (0 < z) -> OrderReflecting (fun y => op y z)} z
    : 0 < z -> forall x y, op x z ≤ op y z -> x ≤ y.
R: Type
H: Le R
H0: Lt R
op: R -> R -> R
Zero0: Zero R
E: forall z : R,
PropHolds (0 < z) ->
OrderReflecting (fun y : R => op y z)
z: R
0 < z -> forall x y : R, op x z ≤ op y z -> x ≤ y
  Proof.
R: Type
H: Le R
H0: Lt R
op: R -> R -> R
Zero0: Zero R
E: forall z : R,
PropHolds (0 < z) ->
OrderReflecting (fun y : R => op y z)
z: R
0 < z -> forall x y : R, op x z ≤ op y z -> x ≤ y
  apply E.
  Qed.

End order_preserving_ops.

Section strict_order_preserving_ops.
  Context `{Lt R}.

  Lemma strictly_order_preserving_flip {op} `{!Commutative op}
    `{!StrictlyOrderPreserving (op z)}
    : StrictlyOrderPreserving (fun y => op y z).
R: Type
H: Lt R
op: R -> R -> R
Commutative0: Commutative op
z: R
StrictlyOrderPreserving0: StrictlyOrderPreserving
  (op z)
StrictlyOrderPreserving (fun y : R => op y z)
  Proof.
R: Type
H: Lt R
op: R -> R -> R
Commutative0: Commutative op
z: R
StrictlyOrderPreserving0: StrictlyOrderPreserving
  (op z)
StrictlyOrderPreserving (fun y : R => op y z)
  intros x y E.
R: Type
H: Lt R
op: R -> R -> R
Commutative0: Commutative op
z: R
StrictlyOrderPreserving0: StrictlyOrderPreserving
  (op z)
x, y: R
E: x < y
op x z < op y z
  rewrite 2!(commutativity _ z).
R: Type
H: Lt R
op: R -> R -> R
Commutative0: Commutative op
z: R
StrictlyOrderPreserving0: StrictlyOrderPreserving
  (op z)
x, y: R
E: x < y
op z x < op z y
  apply strictly_order_preserving;trivial.
  Qed.

  Lemma strictly_order_reflecting_flip {op} `{!Commutative op}
    `{!StrictlyOrderReflecting (op z) }
    : StrictlyOrderReflecting (fun y => op y z).
R: Type
H: Lt R
op: R -> R -> R
Commutative0: Commutative op
z: R
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (op z)
StrictlyOrderReflecting (fun y : R => op y z)
  Proof.
R: Type
H: Lt R
op: R -> R -> R
Commutative0: Commutative op
z: R
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (op z)
StrictlyOrderReflecting (fun y : R => op y z)
  intros x y E.
R: Type
H: Lt R
op: R -> R -> R
Commutative0: Commutative op
z: R
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (op z)
x, y: R
E: op x z < op y z
x < y
  apply (strictly_order_reflecting (op z)).
R: Type
H: Lt R
op: R -> R -> R
Commutative0: Commutative op
z: R
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (op z)
x, y: R
E: op x z < op y z
op z x < op z y
  rewrite 2!(commutativity (f:=op) z).
R: Type
H: Lt R
op: R -> R -> R
Commutative0: Commutative op
z: R
StrictlyOrderReflecting0: StrictlyOrderReflecting
  (op z)
x, y: R
E: op x z < op y z
op x z < op y z
  trivial.
  Qed.

  Lemma strictly_order_preserving_pos (op : R -> R -> R) `{!Zero R}
    {E:forall z, PropHolds (0 < z) -> StrictlyOrderPreserving (op z)} z
    : 0 < z -> forall x y, x < y -> op z x < op z y.
R: Type
H: Lt R
op: R -> R -> R
Zero0: Zero R
E: forall z : R,
PropHolds (0 < z) ->
StrictlyOrderPreserving (op z)
z: R
0 < z -> forall x y : R, x < y -> op z x < op z y
  Proof.
R: Type
H: Lt R
op: R -> R -> R
Zero0: Zero R
E: forall z : R,
PropHolds (0 < z) ->
StrictlyOrderPreserving (op z)
z: R
0 < z -> forall x y : R, x < y -> op z x < op z y
  apply E.
  Qed.

  Lemma strictly_order_preserving_flip_pos (op : R -> R -> R) `{!Zero R}
    {E:forall z, PropHolds (0 < z) -> StrictlyOrderPreserving (fun y => op y z)} z
    : 0 < z -> forall x y, x < y -> op x z < op y z.
R: Type
H: Lt R
op: R -> R -> R
Zero0: Zero R
E: forall z : R,
PropHolds (0 < z) ->
StrictlyOrderPreserving (fun y : R => op y z)
z: R
0 < z -> forall x y : R, x < y -> op x z < op y z
  Proof.
R: Type
H: Lt R
op: R -> R -> R
Zero0: Zero R
E: forall z : R,
PropHolds (0 < z) ->
StrictlyOrderPreserving (fun y : R => op y z)
z: R
0 < z -> forall x y : R, x < y -> op x z < op y z
  apply E.
  Qed.

End strict_order_preserving_ops.

Lemma projected_partial_order `{IsHSet A} {Ale : Le A}
  `{is_mere_relation A Ale} `{Ble : Le B}
  (f : A -> B) `{!IsInjective f} `{!PartialOrder Ble}
  : (forall x y, x ≤ y <-> f x ≤ f y) -> PartialOrder Ale.
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
(forall x y : A, x ≤ y <-> f x ≤ f y) ->
PartialOrder Ale
Proof.
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
(forall x y : A, x ≤ y <-> f x ≤ f y) ->
PartialOrder Ale
intros P.
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
PartialOrder Ale repeat split.
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
IsHSet A
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
is_mere_relation A Ale
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
Reflexive le
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
Transitive le
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
AntiSymmetric le
-
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
IsHSet A exact _.
-
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
is_mere_relation A Ale exact _.
-
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
Reflexive le intros x.
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
x: A
x ≤ x apply P.
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
x: A
f x ≤ f x apply reflexivity.
-
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
Transitive le intros x y z E1 E2.
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
x, y, z: A
E1: x ≤ y
E2: y ≤ z
x ≤ z apply P.
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
x, y, z: A
E1: x ≤ y
E2: y ≤ z
f x ≤ f z
  transitivity (f y); apply P;trivial.
-
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
AntiSymmetric le intros x y E1 E2.
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
x, y: A
E1: x ≤ y
E2: y ≤ x
x = y apply (injective f).
A: Type
IsHSet0: IsHSet A
Ale: Le A
is_mere_relation0: is_mere_relation A Ale
B: Type
Ble: Le B
f: A -> B
IsInjective0: IsInjective f
PartialOrder0: PartialOrder Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
x, y: A
E1: x ≤ y
E2: y ≤ x
f x = f y
  apply (antisymmetry (≤)); apply P;trivial.
Qed.

Lemma projected_total_order `{Ale : Le A} `{Ble : Le B}
  (f : A -> B) `{!TotalRelation Ble}
  : (forall x y, x ≤ y <-> f x ≤ f y) -> TotalRelation Ale.
A: Type
Ale: Le A
B: Type
Ble: Le B
f: A -> B
TotalRelation0: TotalRelation Ble
(forall x y : A, x ≤ y <-> f x ≤ f y) ->
TotalRelation Ale
Proof.
A: Type
Ale: Le A
B: Type
Ble: Le B
f: A -> B
TotalRelation0: TotalRelation Ble
(forall x y : A, x ≤ y <-> f x ≤ f y) ->
TotalRelation Ale
intros P x y.
A: Type
Ale: Le A
B: Type
Ble: Le B
f: A -> B
TotalRelation0: TotalRelation Ble
P: forall x y : A, x ≤ y <-> f x ≤ f y
x, y: A
(Ale x y + Ale y x)%type
destruct (total (≤) (f x) (f y)); [left | right]; apply P;trivial.
Qed.

Lemma projected_strict_order `{Alt : Lt A} `{is_mere_relation A lt} `{Blt : Lt B}
  (f : A -> B) `{!StrictOrder Blt}
  : (forall x y, x < y <-> f x < f y) -> StrictOrder Alt.
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
(forall x y : A, x < y <-> f x < f y) ->
StrictOrder Alt
Proof.
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
(forall x y : A, x < y <-> f x < f y) ->
StrictOrder Alt
intros P.
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
StrictOrder Alt split.
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
is_mere_relation A lt
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
Irreflexive lt
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
Transitive lt
-
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
is_mere_relation A lt exact _.
-
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
Irreflexive lt intros x E.
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
x: A
E: x < x
Empty destruct (irreflexivity (<) (f x)).
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
x: A
E: x < x
f x < f x apply P.
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
x: A
E: x < x
x < x trivial.
-
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
Transitive lt intros x y z E1 E2.
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
x, y, z: A
E1: x < y
E2: y < z
x < z apply P.
A: Type
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
Blt: Lt B
f: A -> B
StrictOrder0: StrictOrder Blt
P: forall x y : A, x < y <-> f x < f y
x, y, z: A
E1: x < y
E2: y < z
f x < f z transitivity (f y); apply P;trivial.
Qed.

Lemma projected_pseudo_order `{IsApart A} `{Alt : Lt A} `{is_mere_relation A lt}
  `{Apart B} `{Blt : Lt B}
  (f : A -> B) `{!IsStrongInjective f} `{!PseudoOrder Blt}
  : (forall x y, x < y <-> f x < f y) -> PseudoOrder Alt.
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
(forall x y : A, x < y <-> f x < f y) ->
PseudoOrder Alt
Proof.
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
(forall x y : A, x < y <-> f x < f y) ->
PseudoOrder Alt
pose proof (strong_injective_mor f).
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
(forall x y : A, x < y <-> f x < f y) ->
PseudoOrder Alt
intros P.
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
PseudoOrder Alt split; try exact _.
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
forall x y : A, ~ (x < y < x)
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
CoTransitive lt
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
forall x y : A, x ≶ y <-> (x < y) + (y < x)
-
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
forall x y : A, ~ (x < y < x) intros x y E.
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: x < y < x
Empty apply (pseudo_order_antisym (f x) (f y)).
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: x < y < x
f x < f y < f x
  split; apply P,E.
-
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
CoTransitive lt intros x y E z.
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: x < y
z: A
hor (x < z) (z < y) apply P in E.
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: f x < f y
z: A
hor (x < z) (z < y)
  apply (merely_destruct (cotransitive E (f z)));
  intros [?|?];apply tr; [left | right]; apply P;trivial.
-
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
forall x y : A, x ≶ y <-> (x < y) + (y < x) intros x y; split; intros E.
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: x ≶ y
((x < y) + (y < x))%type
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: ((x < y) + (y < x))%type
x ≶ y
  +
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: x ≶ y
((x < y) + (y < x))%type apply (strong_injective f) in E.
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: f x ≶ f y
((x < y) + (y < x))%type
    apply apart_iff_total_lt in E.
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: ((f x < f y) + (f y < f x))%type
((x < y) + (y < x))%type
    destruct E; [left | right]; apply P;trivial.
  +
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: ((x < y) + (y < x))%type
x ≶ y apply (strong_extensionality f).
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: ((x < y) + (y < x))%type
f x ≶ f y
    apply apart_iff_total_lt.
A: Type
Aap: Apart A
H: IsApart A
Alt: Lt A
is_mere_relation0: is_mere_relation A lt
B: Type
H0: Apart B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
PseudoOrder0: PseudoOrder Blt
X: StrongExtensionality f
P: forall x y : A, x < y <-> f x < f y
x, y: A
E: ((x < y) + (y < x))%type
((f x < f y) + (f y < f x))%type
    destruct E; [left | right]; apply P;trivial.
Qed.

Lemma projected_full_pseudo_order `{IsApart A} `{Ale : Le A} `{Alt : Lt A}
  `{is_mere_relation A le} `{is_mere_relation A lt}
  `{Apart B} `{Ble : Le B} `{Blt : Lt B}
  (f : A -> B) `{!IsStrongInjective f} `{!FullPseudoOrder Ble Blt}
  : (forall x y, x ≤ y <-> f x ≤ f y) -> (forall x y, x < y <-> f x < f y) ->
    FullPseudoOrder Ale Alt.
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
(forall x y : A, x ≤ y <-> f x ≤ f y) ->
(forall x y : A, x < y <-> f x < f y) ->
FullPseudoOrder Ale Alt
Proof.
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
(forall x y : A, x ≤ y <-> f x ≤ f y) ->
(forall x y : A, x < y <-> f x < f y) ->
FullPseudoOrder Ale Alt
intros P1 P2.
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
FullPseudoOrder Ale Alt split.
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
is_mere_relation A Ale
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
PseudoOrder Alt
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
forall x y : A, x ≤ y <-> ~ (y < x)
-
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
is_mere_relation A Ale exact _.
-
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
PseudoOrder Alt apply (projected_pseudo_order f);assumption.
-
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
forall x y : A, x ≤ y <-> ~ (y < x) intros x y; split; intros E.
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
x, y: A
E: x ≤ y
~ (y < x)
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
x, y: A
E: ~ (y < x)
x ≤ y
  +
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
x, y: A
E: x ≤ y
~ (y < x) intros F.
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
x, y: A
E: x ≤ y
F: y < x
Empty destruct (le_not_lt_flip (f y) (f x));[apply P1|apply P2];trivial.
  +
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
x, y: A
E: ~ (y < x)
x ≤ y apply P1.
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
x, y: A
E: ~ (y < x)
f x ≤ f y apply not_lt_le_flip.
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
x, y: A
E: ~ (y < x)
~ (f y < f x)
    intros F.
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
x, y: A
E: ~ (y < x)
F: f y < f x
Empty apply E,P2.
A: Type
Aap: Apart A
H: IsApart A
Ale: Le A
Alt: Lt A
is_mere_relation0: is_mere_relation A le
is_mere_relation1: is_mere_relation A lt
B: Type
H0: Apart B
Ble: Le B
Blt: Lt B
f: A -> B
IsStrongInjective0: IsStrongInjective f
FullPseudoOrder0: FullPseudoOrder Ble Blt
P1: forall x y : A, x ≤ y <-> f x ≤ f y
P2: forall x y : A, x < y <-> f x < f y
x, y: A
E: ~ (y < x)
F: f y < f x
f y < f x trivial.
Qed.

Instance id_order_preserving `{PartialOrder A} : OrderPreserving (@id A).
A: Type
Ale: Le A
H: PartialOrder Ale
OrderPreserving id
Proof.
A: Type
Ale: Le A
H: PartialOrder Ale
OrderPreserving id
red;trivial.
Qed.

Instance id_order_reflecting `{PartialOrder A} : OrderReflecting (@id A).
A: Type
Ale: Le A
H: PartialOrder Ale
OrderReflecting id
Proof.
A: Type
Ale: Le A
H: PartialOrder Ale
OrderReflecting id
red;trivial.
Qed.

Section composition.
  Context {A B C} `{Le A} `{Le B} `{Le C} (f : A -> B) (g : B -> C).

  Instance compose_order_preserving:
    OrderPreserving f -> OrderPreserving g -> OrderPreserving (g ∘ f).
A, B, C: Type
H: Le A
H0: Le B
H1: Le C
f: A -> B
g: B -> C
OrderPreserving f ->
OrderPreserving g -> OrderPreserving (g ∘ f)
  Proof.
A, B, C: Type
H: Le A
H0: Le B
H1: Le C
f: A -> B
g: B -> C
OrderPreserving f ->
OrderPreserving g -> OrderPreserving (g ∘ f)
  red;intros.
A, B, C: Type
H: Le A
H0: Le B
H1: Le C
f: A -> B
g: B -> C
X: OrderPreserving f
X0: OrderPreserving g
x, y: A
X1: x ≤ y
(g ∘ f) x ≤ (g ∘ f) y unfold Compose.
A, B, C: Type
H: Le A
H0: Le B
H1: Le C
f: A -> B
g: B -> C
X: OrderPreserving f
X0: OrderPreserving g
x, y: A
X1: x ≤ y
g (f x) ≤ g (f y)
  do 2 apply (order_preserving _).
A, B, C: Type
H: Le A
H0: Le B
H1: Le C
f: A -> B
g: B -> C
X: OrderPreserving f
X0: OrderPreserving g
x, y: A
X1: x ≤ y
x ≤ y
  trivial.
  Qed.

  Instance compose_order_reflecting:
    OrderReflecting f -> OrderReflecting g -> OrderReflecting (g ∘ f).
A, B, C: Type
H: Le A
H0: Le B
H1: Le C
f: A -> B
g: B -> C
OrderReflecting f ->
OrderReflecting g -> OrderReflecting (g ∘ f)
  Proof.
A, B, C: Type
H: Le A
H0: Le B
H1: Le C
f: A -> B
g: B -> C
OrderReflecting f ->
OrderReflecting g -> OrderReflecting (g ∘ f)
  intros ?? x y E.
A, B, C: Type
H: Le A
H0: Le B
H1: Le C
f: A -> B
g: B -> C
X: OrderReflecting f
X0: OrderReflecting g
x, y: A
E: (g ∘ f) x ≤ (g ∘ f) y
x ≤ y unfold Compose in E.
A, B, C: Type
H: Le A
H0: Le B
H1: Le C
f: A -> B
g: B -> C
X: OrderReflecting f
X0: OrderReflecting g
x, y: A
E: g (f x) ≤ g (f y)
x ≤ y
  do 2 apply (order_reflecting _) in E.
A, B, C: Type
H: Le A
H0: Le B
H1: Le C
f: A -> B
g: B -> C
X: OrderReflecting f
X0: OrderReflecting g
x, y: A
E: x ≤ y
x ≤ y
  trivial.
  Qed.

  Instance compose_order_embedding:
    OrderEmbedding f -> OrderEmbedding g -> OrderEmbedding (g ∘ f) := {}.
End composition.

#[export]
Hint Extern 4 (OrderPreserving (_ ∘ _)) =>
  class_apply @compose_order_preserving : typeclass_instances.
#[export]
Hint Extern 4 (OrderReflecting (_ ∘ _)) =>
  class_apply @compose_order_reflecting : typeclass_instances.
#[export]
Hint Extern 4 (OrderEmbedding (_ ∘ _)) =>
  class_apply @compose_order_embedding : typeclass_instances.