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

Generalizable Variables K L f.

(*
We prove that the algebraic definition of a lattice corresponds to the
order theoretic one. Note that we do not make any of these instances global,
because that would cause loops.
*)
Section join_semilattice_order.
  Context `{JoinSemiLatticeOrder L}.

  Lemma join_ub_3_r x y z : z ≤ x ⊔ y ⊔ z.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ (x ⊔ y) ⊔ z
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ (x ⊔ y) ⊔ z
  apply join_ub_r.
  Qed.

  Lemma join_ub_3_m x y z : y ≤ x ⊔ y ⊔ z.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ (x ⊔ y) ⊔ z
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ (x ⊔ y) ⊔ z
  transitivity (x ⊔ y).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ x ⊔ y
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ⊔ y ≤ (x ⊔ y) ⊔ z
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ x ⊔ y apply join_ub_r.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ⊔ y ≤ (x ⊔ y) ⊔ z apply join_ub_l.
  Qed.

  Lemma join_ub_3_l x y z : x ≤ x ⊔ y ⊔ z.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ≤ (x ⊔ y) ⊔ z
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ≤ (x ⊔ y) ⊔ z
  transitivity (x ⊔ y); apply join_ub_l.
  Qed.

  Lemma join_ub_3_assoc_l x y z : x ≤ x ⊔ (y ⊔ z).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ≤ x ⊔ (y ⊔ z)
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ≤ x ⊔ (y ⊔ z)
  apply join_ub_l.
  Qed.

  Lemma join_ub_3_assoc_m x y z : y ≤ x ⊔ (y ⊔ z).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ x ⊔ (y ⊔ z)
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ x ⊔ (y ⊔ z)
  transitivity (y ⊔ z).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ y ⊔ z
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ⊔ z ≤ x ⊔ (y ⊔ z)
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ y ⊔ z apply join_ub_l.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ⊔ z ≤ x ⊔ (y ⊔ z) apply join_ub_r.
  Qed.

  Lemma join_ub_3_assoc_r x y z : z ≤ x ⊔ (y ⊔ z).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ x ⊔ (y ⊔ z)
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ x ⊔ (y ⊔ z)
  transitivity (y ⊔ z); apply join_ub_r.
  Qed.

  Instance join_sl_order_join_sl: IsJoinSemiLattice L.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
IsJoinSemiLattice L
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
IsJoinSemiLattice L
  repeat split.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
IsHSet L
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
Associative sg_op
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
Commutative sg_op
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
BinaryIdempotent sg_op
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
IsHSet L exact _.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
Associative sg_op intros x y z.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) = sg_op (sg_op x y) z apply (antisymmetry (≤)).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ sg_op (sg_op x y) z
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ sg_op x (sg_op y z)
    +
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ sg_op (sg_op x y) z apply join_lub.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ≤ sg_op (sg_op x y) z
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
sg_op y z ≤ sg_op (sg_op x y) z
      *
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ≤ sg_op (sg_op x y) z apply join_ub_3_l.
      *
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
sg_op y z ≤ sg_op (sg_op x y) z apply join_lub.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ sg_op (sg_op x y) z
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ sg_op (sg_op x y) z
        **
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ sg_op (sg_op x y) z apply join_ub_3_m.
        **
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ sg_op (sg_op x y) z apply join_ub_3_r.
    +
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ sg_op x (sg_op y z) apply join_lub.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
sg_op x y ≤ sg_op x (sg_op y z)
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ sg_op x (sg_op y z)
      *
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
sg_op x y ≤ sg_op x (sg_op y z) apply join_lub.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ≤ sg_op x (sg_op y z)
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ sg_op x (sg_op y z)
        **
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ≤ sg_op x (sg_op y z) apply join_ub_3_assoc_l.
        **
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
y ≤ sg_op x (sg_op y z) apply join_ub_3_assoc_m.
      *
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ sg_op x (sg_op y z) apply join_ub_3_assoc_r.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
Commutative sg_op intros x y.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
sg_op x y = sg_op y x apply (antisymmetry (≤)); apply join_lub;
    first [apply join_ub_l | apply join_ub_r].
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
BinaryIdempotent sg_op intros x.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
Idempotent sg_op x red.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
sg_op x x = x apply (antisymmetry (≤)).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
sg_op x x ≤ x
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
x ≤ sg_op x x
    +
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
sg_op x x ≤ x apply join_lub; apply reflexivity.
    +
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
x ≤ sg_op x x apply join_ub_l.
  Qed.

  Lemma join_le_compat_r x y z : z ≤ x -> z ≤ x ⊔ y.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ x -> z ≤ x ⊔ y
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ x -> z ≤ x ⊔ y
  intros E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
E: z ≤ x
z ≤ x ⊔ y transitivity x.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
E: z ≤ x
z ≤ x
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
E: z ≤ x
x ≤ x ⊔ y
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
E: z ≤ x
z ≤ x trivial.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
E: z ≤ x
x ≤ x ⊔ y apply join_ub_l.
  Qed.

  Lemma join_le_compat_l x y z : z ≤ y -> z ≤ x ⊔ y.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ y -> z ≤ x ⊔ y
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
z ≤ y -> z ≤ x ⊔ y
  intros E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
E: z ≤ y
z ≤ x ⊔ y rewrite (commutativity (f:=join)).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
E: z ≤ y
z ≤ y ⊔ x
  apply join_le_compat_r.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
E: z ≤ y
z ≤ y
  trivial.
  Qed.

  Lemma join_l x y : y ≤ x -> x ⊔ y = x.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
y ≤ x -> x ⊔ y = x
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
y ≤ x -> x ⊔ y = x
  intros E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: y ≤ x
x ⊔ y = x apply (antisymmetry (≤)).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: y ≤ x
x ⊔ y ≤ x
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: y ≤ x
x ≤ x ⊔ y
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: y ≤ x
x ⊔ y ≤ x apply join_lub;trivial.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: y ≤ x
x ≤ x apply reflexivity.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: y ≤ x
x ≤ x ⊔ y apply join_ub_l.
  Qed.

  Lemma join_r x y : x ≤ y -> x ⊔ y = y.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
x ≤ y -> x ⊔ y = y
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
x ≤ y -> x ⊔ y = y
  intros E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ⊔ y = y rewrite (commutativity (f:=join)).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: x ≤ y
y ⊔ x = y
  apply join_l.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ≤ y
  trivial.
  Qed.

  Lemma join_sl_le_spec x y : x ≤ y <-> x ⊔ y = y.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
x ≤ y <-> x ⊔ y = y
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
x ≤ y <-> x ⊔ y = y
  split; intros E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ⊔ y = y
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: x ⊔ y = y
x ≤ y
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ⊔ y = y apply join_r.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ≤ y trivial.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: x ⊔ y = y
x ≤ y rewrite <-E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y: L
E: x ⊔ y = y
x ≤ x ⊔ y apply join_ub_l.
  Qed.

  #[export] Instance join_le_preserving_l : forall z, OrderPreserving (z ⊔).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
forall z : L, OrderPreserving (join z)
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
forall z : L, OrderPreserving (join z)
  red;intros.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
z ⊔ x ≤ z ⊔ y
  apply join_lub.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
z ≤ z ⊔ y
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
x ≤ z ⊔ y
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
z ≤ z ⊔ y apply join_ub_l.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
x ≤ z ⊔ y apply join_le_compat_l.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
x ≤ y trivial.
  Qed.

  #[export] Instance join_le_preserving_r : forall z, OrderPreserving (⊔ z).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
forall z : L, OrderPreserving (fun Y : L => Y ⊔ z)
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
forall z : L, OrderPreserving (fun Y : L => Y ⊔ z)
  intros.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
z: L
OrderPreserving (fun Y : L => Y ⊔ z) exact maps.order_preserving_flip.
  Qed.

  Lemma join_le_compat x₁ x₂ y₁ y₂ : x₁ ≤ x₂ -> y₁ ≤ y₂ -> x₁ ⊔ y₁ ≤ x₂ ⊔ y₂.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
x₁ ≤ x₂ -> y₁ ≤ y₂ -> x₁ ⊔ y₁ ≤ x₂ ⊔ y₂
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
x₁ ≤ x₂ -> y₁ ≤ y₂ -> x₁ ⊔ y₁ ≤ x₂ ⊔ y₂
  intros E1 E2.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
x₁ ⊔ y₁ ≤ x₂ ⊔ y₂ transitivity (x₁ ⊔ y₂).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
x₁ ⊔ y₁ ≤ x₁ ⊔ y₂
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
x₁ ⊔ y₂ ≤ x₂ ⊔ y₂
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
x₁ ⊔ y₁ ≤ x₁ ⊔ y₂ apply (order_preserving (x₁ ⊔)).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
y₁ ≤ y₂ trivial.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
x₁ ⊔ y₂ ≤ x₂ ⊔ y₂ apply (order_preserving (⊔ y₂));trivial.
  Qed.

  Lemma join_le x y z : x ≤ z -> y ≤ z -> x ⊔ y ≤ z.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ≤ z -> y ≤ z -> x ⊔ y ≤ z
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x, y, z: L
x ≤ z -> y ≤ z -> x ⊔ y ≤ z
    apply join_lub.
  Qed.

  Section total_join.
  Context `{!TotalRelation le}.

  Lemma total_join_either `{!TotalRelation le} x y : join x y = x |_| join x y = y.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0, TotalRelation1: TotalRelation le
x, y: L
((x ⊔ y = x) + (x ⊔ y = y))%type
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0, TotalRelation1: TotalRelation le
x, y: L
((x ⊔ y = x) + (x ⊔ y = y))%type
  destruct (total le x y) as [E|E].
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0, TotalRelation1: TotalRelation le
x, y: L
E: x ≤ y
((x ⊔ y = x) + (x ⊔ y = y))%type
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0, TotalRelation1: TotalRelation le
x, y: L
E: y ≤ x
((x ⊔ y = x) + (x ⊔ y = y))%type
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0, TotalRelation1: TotalRelation le
x, y: L
E: x ≤ y
((x ⊔ y = x) + (x ⊔ y = y))%type right.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0, TotalRelation1: TotalRelation le
x, y: L
E: x ≤ y
x ⊔ y = y apply join_r,E.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0, TotalRelation1: TotalRelation le
x, y: L
E: y ≤ x
((x ⊔ y = x) + (x ⊔ y = y))%type left.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0, TotalRelation1: TotalRelation le
x, y: L
E: y ≤ x
x ⊔ y = x apply join_l,E.
  Qed.

  Definition max x y :=
    match total le x y with
    | inl _ => y
    | inr _ => x
    end.

  Lemma total_join_max x y : join x y = max x y.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
x ⊔ y = max x y
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
x ⊔ y = max x y
  unfold max;destruct (total le x y) as [E|E].
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: x ≤ y
x ⊔ y = y
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: y ≤ x
x ⊔ y = x
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: x ≤ y
x ⊔ y = y apply join_r,E.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: y ≤ x
x ⊔ y = x apply join_l,E.
  Qed.
  End total_join.

  Lemma join_idempotent x : x ⊔ x = x.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
x ⊔ x = x
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
x ⊔ x = x
    assert (le1 : x ⊔ x ≤ x).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
x ⊔ x ≤ x
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
le1: x ⊔ x ≤ x
x ⊔ x = x
    {
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
x ⊔ x ≤ x
      refine (join_lub _ _ _ _ _); apply reflexivity.
    }
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
le1: x ⊔ x ≤ x
x ⊔ x = x
    assert (le2 : x ≤ x ⊔ x).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
le1: x ⊔ x ≤ x
x ≤ x ⊔ x
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
le1: x ⊔ x ≤ x
le2: x ≤ x ⊔ x
x ⊔ x = x
    {
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
le1: x ⊔ x ≤ x
x ≤ x ⊔ x
      exact (join_ub_l _ _).
    }
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
x: L
le1: x ⊔ x ≤ x
le2: x ≤ x ⊔ x
x ⊔ x = x
    exact (antisymmetry _ _ _ le1 le2).
  Qed.
End join_semilattice_order.

Section bounded_join_semilattice.
  Context `{JoinSemiLatticeOrder L} `{Bottom L} `{!IsBoundedJoinSemiLattice L}.

  Lemma above_bottom x : ⊥ ≤ x.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
H1: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
⊥ ≤ x
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
H1: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
⊥ ≤ x
  apply join_sl_le_spec.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
H1: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
⊥ ⊔ x = x
  rewrite left_identity.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
H1: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
x = x
  reflexivity.
  Qed.

  Lemma below_bottom x : x ≤ ⊥ -> x = ⊥.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
H1: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
x ≤ ⊥ -> x = ⊥
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
H1: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
x ≤ ⊥ -> x = ⊥
  intros E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
H1: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
E: x ≤ ⊥
x = ⊥
  apply join_sl_le_spec in E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
H1: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
E: x ⊔ ⊥ = ⊥
x = ⊥ rewrite right_identity in E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
H1: Bottom L
IsBoundedJoinSemiLattice0: IsBoundedJoinSemiLattice L
x: L
E: x = ⊥
x = ⊥
  trivial.
  Qed.
End bounded_join_semilattice.

Section meet_semilattice_order.
  Context `{MeetSemiLatticeOrder L}.

  Lemma meet_lb_3_r x y z : x ⊓ y ⊓ z ≤ z.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊓ z ≤ z
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊓ z ≤ z
  apply meet_lb_r.
  Qed.

  Lemma meet_lb_3_m x y z : x ⊓ y ⊓ z ≤ y.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊓ z ≤ y
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊓ z ≤ y
  transitivity (x ⊓ y).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊓ z ≤ x ⊓ y
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ⊓ y ≤ y
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊓ z ≤ x ⊓ y apply meet_lb_l.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ⊓ y ≤ y apply meet_lb_r.
  Qed.

  Lemma meet_lb_3_l x y z : x ⊓ y ⊓ z ≤ x.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊓ z ≤ x
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊓ z ≤ x
  transitivity (x ⊓ y); apply meet_lb_l.
  Qed.

  Lemma meet_lb_3_assoc_l x y z : x ⊓ (y ⊓ z) ≤ x.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ⊓ (y ⊓ z) ≤ x
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ⊓ (y ⊓ z) ≤ x
  apply meet_lb_l.
  Qed.

  Lemma meet_lb_3_assoc_m x y z : x ⊓ (y ⊓ z) ≤ y.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ⊓ (y ⊓ z) ≤ y
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ⊓ (y ⊓ z) ≤ y
  transitivity (y ⊓ z).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ⊓ (y ⊓ z) ≤ y ⊓ z
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
y ⊓ z ≤ y
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ⊓ (y ⊓ z) ≤ y ⊓ z apply meet_lb_r.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
y ⊓ z ≤ y apply meet_lb_l.
  Qed.

  Lemma meet_lb_3_assoc_r x y z : x ⊓ (y ⊓ z) ≤ z.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ⊓ (y ⊓ z) ≤ z
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ⊓ (y ⊓ z) ≤ z
  transitivity (y ⊓ z); apply meet_lb_r.
  Qed.

  Instance meet_sl_order_meet_sl: IsMeetSemiLattice L.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
IsMeetSemiLattice L
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
IsMeetSemiLattice L
  repeat split.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
IsHSet L
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
Associative sg_op
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
Commutative sg_op
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
BinaryIdempotent sg_op
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
IsHSet L exact _.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
Associative sg_op intros x y z.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) = sg_op (sg_op x y) z apply (antisymmetry (≤)).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ sg_op (sg_op x y) z
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ sg_op x (sg_op y z)
    +
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ sg_op (sg_op x y) z apply meet_glb.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ sg_op x y
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ z
      *
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ sg_op x y apply meet_glb.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ x
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ y
        **
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ x apply meet_lb_3_assoc_l.
        **
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ y apply meet_lb_3_assoc_m.
      *
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op x (sg_op y z) ≤ z apply meet_lb_3_assoc_r.
    +
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ sg_op x (sg_op y z) apply meet_glb.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ x
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ sg_op y z
      **
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ x apply meet_lb_3_l.
      **
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ sg_op y z apply meet_glb.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ y
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ z
         ***
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ y apply meet_lb_3_m.
         ***
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
sg_op (sg_op x y) z ≤ z apply meet_lb_3_r.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
Commutative sg_op intros x y.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
sg_op x y = sg_op y x apply (antisymmetry (≤)); apply meet_glb;
    first [apply meet_lb_l | try apply meet_lb_r].
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
BinaryIdempotent sg_op intros x.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
Idempotent sg_op x red.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
sg_op x x = x apply (antisymmetry (≤)).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
sg_op x x ≤ x
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
x ≤ sg_op x x
    +
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
sg_op x x ≤ x apply meet_lb_l.
    +
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
x ≤ sg_op x x apply meet_glb;apply reflexivity.
  Qed.

  Lemma meet_le_compat_r x y z : x ≤ z -> x ⊓ y ≤ z.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ≤ z -> x ⊓ y ≤ z
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
x ≤ z -> x ⊓ y ≤ z
  intros E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
E: x ≤ z
x ⊓ y ≤ z transitivity x.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
E: x ≤ z
x ⊓ y ≤ x
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
E: x ≤ z
x ≤ z
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
E: x ≤ z
x ⊓ y ≤ x apply meet_lb_l.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
E: x ≤ z
x ≤ z trivial.
  Qed.

  Lemma meet_le_compat_l x y z : y ≤ z -> x ⊓ y ≤ z.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
y ≤ z -> x ⊓ y ≤ z
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
y ≤ z -> x ⊓ y ≤ z
  intros E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
E: y ≤ z
x ⊓ y ≤ z rewrite (commutativity (f:=meet)).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
E: y ≤ z
y ⊓ x ≤ z
  apply meet_le_compat_r.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
E: y ≤ z
y ≤ z
  trivial.
  Qed.

  Lemma meet_l x y : x ≤ y -> x ⊓ y = x.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
x ≤ y -> x ⊓ y = x
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
x ≤ y -> x ⊓ y = x
  intros E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ⊓ y = x apply (antisymmetry (≤)).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ⊓ y ≤ x
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ≤ x ⊓ y
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ⊓ y ≤ x apply meet_lb_l.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ≤ x ⊓ y apply meet_glb; trivial.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ≤ x apply reflexivity.
  Qed.

  Lemma meet_r x y : y ≤ x -> x ⊓ y = y.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
y ≤ x -> x ⊓ y = y
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
y ≤ x -> x ⊓ y = y
  intros E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: y ≤ x
x ⊓ y = y rewrite (commutativity (f:=meet)).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: y ≤ x
y ⊓ x = y apply meet_l.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: y ≤ x
y ≤ x
  trivial.
  Qed.

  Lemma meet_sl_le_spec x y : x ≤ y <-> x ⊓ y = x.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
x ≤ y <-> x ⊓ y = x
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
x ≤ y <-> x ⊓ y = x
  split; intros E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ⊓ y = x
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: x ⊓ y = x
x ≤ y
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: x ≤ y
x ⊓ y = x apply meet_l;trivial.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: x ⊓ y = x
x ≤ y rewrite <-E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y: L
E: x ⊓ y = x
x ⊓ y ≤ y apply meet_lb_r.
  Qed.

  #[export] Instance orderpreserving_left_meet : forall z, OrderPreserving (z ⊓).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
forall z : L, OrderPreserving (meet z)
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
forall z : L, OrderPreserving (meet z)
  red;intros.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
z ⊓ x ≤ z ⊓ y
  apply meet_glb.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
z ⊓ x ≤ z
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
z ⊓ x ≤ y
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
z ⊓ x ≤ z apply meet_lb_l.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
z ⊓ x ≤ y apply  meet_le_compat_l.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
z, x, y: L
X: x ≤ y
x ≤ y trivial.
  Qed.

  #[export] Instance orderpreserving_right_meet: forall z, OrderPreserving (⊓ z).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
forall z : L, OrderPreserving (fun Y : L => Y ⊓ z)
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
forall z : L, OrderPreserving (fun Y : L => Y ⊓ z)
  intros.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
z: L
OrderPreserving (fun Y : L => Y ⊓ z) exact maps.order_preserving_flip.
  Qed.

  Lemma meet_le_compat x₁ x₂ y₁ y₂ : x₁ ≤ x₂ -> y₁ ≤ y₂ -> x₁ ⊓ y₁ ≤ x₂ ⊓ y₂.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
x₁ ≤ x₂ -> y₁ ≤ y₂ -> x₁ ⊓ y₁ ≤ x₂ ⊓ y₂
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
x₁ ≤ x₂ -> y₁ ≤ y₂ -> x₁ ⊓ y₁ ≤ x₂ ⊓ y₂
  intros E1 E2.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
x₁ ⊓ y₁ ≤ x₂ ⊓ y₂ transitivity (x₁ ⊓ y₂).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
x₁ ⊓ y₁ ≤ x₁ ⊓ y₂
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
x₁ ⊓ y₂ ≤ x₂ ⊓ y₂
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
x₁ ⊓ y₁ ≤ x₁ ⊓ y₂ apply (order_preserving (x₁ ⊓)).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
y₁ ≤ y₂ trivial.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
x₁ ⊓ y₂ ≤ x₂ ⊓ y₂ apply (order_preserving (⊓ y₂)).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x₁, x₂, y₁, y₂: L
E1: x₁ ≤ x₂
E2: y₁ ≤ y₂
x₁ ≤ x₂ trivial.
  Qed.

  Lemma meet_le x y z : z ≤ x -> z ≤ y -> z ≤ x ⊓ y.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
z ≤ x -> z ≤ y -> z ≤ x ⊓ y
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x, y, z: L
z ≤ x -> z ≤ y -> z ≤ x ⊓ y
    apply meet_glb.
  Qed.

  Section total_meet.
  Context `{!TotalRelation le}.

  Lemma total_meet_either x y : meet x y = x |_| meet x y = y.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
((x ⊓ y = x) + (x ⊓ y = y))%type
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
((x ⊓ y = x) + (x ⊓ y = y))%type
  destruct (total le x y) as [E|E].
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: x ≤ y
((x ⊓ y = x) + (x ⊓ y = y))%type
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: y ≤ x
((x ⊓ y = x) + (x ⊓ y = y))%type
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: x ≤ y
((x ⊓ y = x) + (x ⊓ y = y))%type left.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: x ≤ y
x ⊓ y = x apply meet_l,E.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: y ≤ x
((x ⊓ y = x) + (x ⊓ y = y))%type right.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: y ≤ x
x ⊓ y = y apply meet_r,E.
  Qed.

  Definition min x y :=
    match total le x y with
    | inr _ => y
    | inl _ => x
    end.

  Lemma total_meet_min x y : meet x y = min x y.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
x ⊓ y = min x y
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
x ⊓ y = min x y
  unfold min.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
x ⊓ y =
match total le x y with
| inl _ => x
| inr _ => y
end destruct (total le x y) as [E|E].
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: x ≤ y
x ⊓ y = x
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: y ≤ x
x ⊓ y = y
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: x ≤ y
x ⊓ y = x apply meet_l,E.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
TotalRelation0: TotalRelation le
x, y: L
E: y ≤ x
x ⊓ y = y apply meet_r,E.
  Qed.
  End total_meet.

  Lemma meet_idempotent x : x ⊓ x = x.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
x ⊓ x = x
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
x ⊓ x = x
    assert (le1 : x ⊓ x ≤ x).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
x ⊓ x ≤ x
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
le1: x ⊓ x ≤ x
x ⊓ x = x
    {
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
x ⊓ x ≤ x
      exact (meet_lb_l _ _).
    }
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
le1: x ⊓ x ≤ x
x ⊓ x = x
    assert (le2 : x ≤ x ⊓ x).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
le1: x ⊓ x ≤ x
x ≤ x ⊓ x
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
le1: x ⊓ x ≤ x
le2: x ≤ x ⊓ x
x ⊓ x = x
    {
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
le1: x ⊓ x ≤ x
x ≤ x ⊓ x
      refine (meet_glb _ _ _ _ _); apply reflexivity.
    }
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
x: L
le1: x ⊓ x ≤ x
le2: x ≤ x ⊓ x
x ⊓ x = x
    exact (antisymmetry _ _ _ le1 le2).
  Qed.

End meet_semilattice_order.

Section lattice_order.
  Context `{LatticeOrder L}.

  Instance isjoinsemilattice_latticeorder : IsJoinSemiLattice L := join_sl_order_join_sl.
  Instance ismeetsemilattice_latticeorder : IsMeetSemiLattice L := meet_sl_order_meet_sl.

  Instance absorption_join_meet : Absorption (⊓) (⊔).
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
Absorption meet join
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
Absorption meet join
  intros x y.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ⊓ (x ⊔ y) = x apply (antisymmetry (≤)).
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ⊓ (x ⊔ y) ≤ x
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ≤ x ⊓ (x ⊔ y)
  -
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ⊓ (x ⊔ y) ≤ x apply meet_lb_l.
  -
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ≤ x ⊓ (x ⊔ y) apply meet_le.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ≤ x
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ≤ x ⊔ y
   +
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ≤ x apply reflexivity.
   +
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ≤ x ⊔ y apply join_ub_l.
  Qed.

  Instance absorption_meet_join : Absorption (⊔) (⊓).
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
Absorption join meet
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
Absorption join meet
  intros x y.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ⊔ (x ⊓ y) = x apply (antisymmetry (≤)).
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ⊔ (x ⊓ y) ≤ x
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ≤ x ⊔ (x ⊓ y)
  -
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ⊔ (x ⊓ y) ≤ x apply join_le.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ≤ x
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ⊓ y ≤ x
    +
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ≤ x apply reflexivity.
    +
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ⊓ y ≤ x apply meet_lb_l.
  -
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y: L
x ≤ x ⊔ (x ⊓ y) apply join_ub_l.
  Qed.

  Instance lattice_order_lattice: IsLattice L := {}.

  Lemma meet_join_distr_l_le x y z : (x ⊓ y) ⊔ (x ⊓ z) ≤ x ⊓ (y ⊔ z).
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊔ (x ⊓ z) ≤ x ⊓ (y ⊔ z)
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊔ (x ⊓ z) ≤ x ⊓ (y ⊔ z)
  apply meet_le.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊔ (x ⊓ z) ≤ x
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊔ (x ⊓ z) ≤ y ⊔ z
  -
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊔ (x ⊓ z) ≤ x apply join_le; apply meet_lb_l.
  -
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
(x ⊓ y) ⊔ (x ⊓ z) ≤ y ⊔ z apply join_le.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊓ y ≤ y ⊔ z
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊓ z ≤ y ⊔ z
    +
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊓ y ≤ y ⊔ z transitivity y.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊓ y ≤ y
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ≤ y ⊔ z
      *
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊓ y ≤ y apply meet_lb_r.
      *
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ≤ y ⊔ z apply join_ub_l.
    +
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊓ z ≤ y ⊔ z transitivity z.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊓ z ≤ z
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
z ≤ y ⊔ z
      *
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊓ z ≤ z apply meet_lb_r.
      *
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
z ≤ y ⊔ z apply join_ub_r.
  Qed.

  Lemma join_meet_distr_l_le x y z : x ⊔ (y ⊓ z) ≤ (x ⊔ y) ⊓ (x ⊔ z).
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊔ (y ⊓ z) ≤ (x ⊔ y) ⊓ (x ⊔ z)
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊔ (y ⊓ z) ≤ (x ⊔ y) ⊓ (x ⊔ z)
  apply meet_le.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊔ (y ⊓ z) ≤ x ⊔ y
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊔ (y ⊓ z) ≤ x ⊔ z
  -
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊔ (y ⊓ z) ≤ x ⊔ y apply join_le.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ≤ x ⊔ y
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ⊓ z ≤ x ⊔ y
    +
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ≤ x ⊔ y apply join_ub_l.
    +
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ⊓ z ≤ x ⊔ y transitivity y.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ⊓ z ≤ y
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ≤ x ⊔ y
      *
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ⊓ z ≤ y apply meet_lb_l.
      *
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ≤ x ⊔ y apply join_ub_r.
  -
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ⊔ (y ⊓ z) ≤ x ⊔ z apply join_le.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ≤ x ⊔ z
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ⊓ z ≤ x ⊔ z
    +
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
x ≤ x ⊔ z apply join_ub_l.
    +
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ⊓ z ≤ x ⊔ z transitivity z.
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ⊓ z ≤ z
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
z ≤ x ⊔ z
      *
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
y ⊓ z ≤ z apply meet_lb_r.
      *
L: Type
Ale: Le L
H: Meet L
H0: Join L
H1: LatticeOrder Ale
x, y, z: L
z ≤ x ⊔ z apply join_ub_r.
  Qed.
End lattice_order.

Definition default_join_sl_le `{IsJoinSemiLattice L} : Le L :=  fun x y => x ⊔ y = y.

Section join_sl_order_alt.
  Context `{IsJoinSemiLattice L} `{Le L} `{is_mere_relation L le}
    (le_correct : forall x y, x ≤ y <-> x ⊔ y = y).

  Lemma alt_Build_JoinSemiLatticeOrder : JoinSemiLatticeOrder (≤).
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
JoinSemiLatticeOrder le
  Proof.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
JoinSemiLatticeOrder le
  repeat split.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
IsHSet L
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
is_mere_relation L le
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
Reflexive le
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
Transitive le
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
AntiSymmetric le
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
forall x y : L, x ≤ x ⊔ y
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
forall x y : L, y ≤ x ⊔ y
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
forall x y z : L, x ≤ z -> y ≤ z -> x ⊔ y ≤ z
  -
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
IsHSet L exact _.
  -
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
is_mere_relation L le exact _.
  -
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
Reflexive le intros x.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x: L
x ≤ x
    apply le_correct.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x: L
x ⊔ x = x apply binary_idempotent.
  -
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
Transitive le intros x y z E1 E2.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y, z: L
E1: x ≤ y
E2: y ≤ z
x ≤ z
    apply le_correct in E1;apply le_correct in E2;apply le_correct.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y, z: L
E1: x ⊔ y = y
E2: y ⊔ z = z
x ⊔ z = z
    rewrite <-E2, simple_associativity, E1.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y, z: L
E1: x ⊔ y = y
E2: y ⊔ z = z
y ⊔ z = y ⊔ z reflexivity.
  -
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
AntiSymmetric le intros x y E1 E2.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y: L
E1: x ≤ y
E2: y ≤ x
x = y
    apply le_correct in E1;apply le_correct in E2.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y: L
E1: x ⊔ y = y
E2: y ⊔ x = x
x = y
    rewrite <-E1, (commutativity (f:=join)).
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y: L
E1: x ⊔ y = y
E2: y ⊔ x = x
x = y ⊔ x
    apply symmetry;trivial.
  -
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
forall x y : L, x ≤ x ⊔ y intros.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y: L
x ≤ x ⊔ y apply le_correct.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y: L
x ⊔ (x ⊔ y) = x ⊔ y
    rewrite simple_associativity,binary_idempotent.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y: L
x ⊔ y = x ⊔ y
    reflexivity.
  -
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
forall x y : L, y ≤ x ⊔ y intros;apply le_correct.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y: L
y ⊔ (x ⊔ y) = x ⊔ y
    rewrite (commutativity (f:=join)).
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y: L
(x ⊔ y) ⊔ y = x ⊔ y
    rewrite <-simple_associativity.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y: L
x ⊔ (y ⊔ y) = x ⊔ y
    rewrite (idempotency _ _).
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y: L
x ⊔ y = x ⊔ y
    reflexivity.
  -
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
forall x y z : L, x ≤ z -> y ≤ z -> x ⊔ y ≤ z intros x y z E1 E2.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y, z: L
E1: x ≤ z
E2: y ≤ z
x ⊔ y ≤ z
    apply le_correct in E1;apply le_correct in E2;apply le_correct.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y, z: L
E1: x ⊔ z = z
E2: y ⊔ z = z
(x ⊔ y) ⊔ z = z
    rewrite <-simple_associativity, E2.
L: Type
Ajoin: Join L
H: IsJoinSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊔ y = y
x, y, z: L
E1: x ⊔ z = z
E2: y ⊔ z = z
x ⊔ z = z trivial.
  Qed.
End join_sl_order_alt.

Definition default_meet_sl_le `{IsMeetSemiLattice L} : Le L :=  fun x y => x ⊓ y = x.

Section meet_sl_order_alt.
  Context `{IsMeetSemiLattice L} `{Le L} `{is_mere_relation L le}
    (le_correct : forall x y, x ≤ y <-> x ⊓ y = x).

  Lemma alt_Build_MeetSemiLatticeOrder : MeetSemiLatticeOrder (≤).
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
MeetSemiLatticeOrder le
  Proof.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
MeetSemiLatticeOrder le
  repeat split.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
IsHSet L
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
is_mere_relation L le
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
Reflexive le
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
Transitive le
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
AntiSymmetric le
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
forall x y : L, x ⊓ y ≤ x
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
forall x y : L, x ⊓ y ≤ y
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
forall x y z : L, z ≤ x -> z ≤ y -> z ≤ x ⊓ y
  -
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
IsHSet L exact _.
  -
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
is_mere_relation L le exact _.
  -
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
Reflexive le intros ?.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x: L
x ≤ x apply le_correct.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x: L
x ⊓ x = x exact (idempotency _ _).
  -
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
Transitive le intros ? ? ? E1 E2.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y, z: L
E1: x ≤ y
E2: y ≤ z
x ≤ z
    apply le_correct in E1;apply le_correct in E2;apply le_correct.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y, z: L
E1: x ⊓ y = x
E2: y ⊓ z = y
x ⊓ z = x
    rewrite <-E1, <-simple_associativity, E2.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y, z: L
E1: x ⊓ y = x
E2: y ⊓ z = y
x ⊓ y = x ⊓ y
    reflexivity.
  -
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
AntiSymmetric le intros ? ? E1 E2.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y: L
E1: x ≤ y
E2: y ≤ x
x = y
    apply le_correct in E1;apply le_correct in E2.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y: L
E1: x ⊓ y = x
E2: y ⊓ x = y
x = y
    rewrite <-E2, (commutativity (f:=meet)).
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y: L
E1: x ⊓ y = x
E2: y ⊓ x = y
x = x ⊓ y
    apply symmetry,E1.
  -
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
forall x y : L, x ⊓ y ≤ x intros ? ?.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y: L
x ⊓ y ≤ x apply le_correct.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y: L
(x ⊓ y) ⊓ x = x ⊓ y
    rewrite (commutativity (f:=meet)), simple_associativity, (idempotency _ _).
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y: L
x ⊓ y = x ⊓ y
    reflexivity.
  -
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
forall x y : L, x ⊓ y ≤ y intros ? ?.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y: L
x ⊓ y ≤ y apply le_correct.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y: L
(x ⊓ y) ⊓ y = x ⊓ y
    rewrite <-simple_associativity, (idempotency _ _).
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y: L
x ⊓ y = x ⊓ y
    reflexivity.
  -
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
forall x y z : L, z ≤ x -> z ≤ y -> z ≤ x ⊓ y intros ? ? ? E1 E2.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y, z: L
E1: z ≤ x
E2: z ≤ y
z ≤ x ⊓ y
    apply le_correct in E1;apply le_correct in E2;apply le_correct.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y, z: L
E1: z ⊓ x = z
E2: z ⊓ y = z
z ⊓ (x ⊓ y) = z
    rewrite associativity, E1.
L: Type
Ameet: Meet L
H: IsMeetSemiLattice L
H0: Le L
is_mere_relation0: is_mere_relation L le
le_correct: forall x y : L, x ≤ y <-> x ⊓ y = x
x, y, z: L
E1: z ⊓ x = z
E2: z ⊓ y = z
z ⊓ y = z
    trivial.
  Qed.
End meet_sl_order_alt.

Section join_order_preserving.
  Context `{JoinSemiLatticeOrder L} `{JoinSemiLatticeOrder K} (f : L -> K)
    `{!IsJoinPreserving f}.

  Lemma join_sl_mor_preserving: OrderPreserving f.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
OrderPreserving f
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
OrderPreserving f
  intros x y E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
x, y: L
E: x ≤ y
f x ≤ f y
  apply join_sl_le_spec in E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
x, y: L
E: x ⊔ y = y
f x ≤ f y apply join_sl_le_spec.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
x, y: L
E: x ⊔ y = y
f x ⊔ f y = f y
  rewrite <-preserves_join.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
x, y: L
E: x ⊔ y = y
f (x ⊔ y) = f y
  apply ap, E.
  Qed.

  Lemma join_sl_mor_reflecting `{!IsInjective f}: OrderReflecting f.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
IsInjective0: IsInjective f
OrderReflecting f
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
IsInjective0: IsInjective f
OrderReflecting f
  intros x y E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
IsInjective0: IsInjective f
x, y: L
E: f x ≤ f y
x ≤ y
  apply join_sl_le_spec in E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
IsInjective0: IsInjective f
x, y: L
E: f x ⊔ f y = f y
x ≤ y apply join_sl_le_spec.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
IsInjective0: IsInjective f
x, y: L
E: f x ⊔ f y = f y
x ⊔ y = y
  rewrite <-preserves_join in E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
IsInjective0: IsInjective f
x, y: L
E: f (x ⊔ y) = f y
x ⊔ y = y
  apply (injective f).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
f: L -> K
IsJoinPreserving0: IsJoinPreserving f
IsInjective0: IsInjective f
x, y: L
E: f (x ⊔ y) = f y
f (x ⊔ y) = f y assumption.
  Qed.
End join_order_preserving.

Section meet_order_preserving.
  Context `{MeetSemiLatticeOrder L} `{MeetSemiLatticeOrder K} (f : L -> K)
    `{!IsMeetPreserving f}.

  Lemma meet_sl_mor_preserving: OrderPreserving f.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
OrderPreserving f
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
OrderPreserving f
  intros x y E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
x, y: L
E: x ≤ y
f x ≤ f y
  apply meet_sl_le_spec in E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
x, y: L
E: x ⊓ y = x
f x ≤ f y apply meet_sl_le_spec.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
x, y: L
E: x ⊓ y = x
f x ⊓ f y = f x
  rewrite <-preserves_meet.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
x, y: L
E: x ⊓ y = x
f (x ⊓ y) = f x
  apply ap, E.
  Qed.

  Lemma meet_sl_mor_reflecting `{!IsInjective f}: OrderReflecting f.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
IsInjective0: IsInjective f
OrderReflecting f
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
IsInjective0: IsInjective f
OrderReflecting f
  intros x y E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
IsInjective0: IsInjective f
x, y: L
E: f x ≤ f y
x ≤ y
  apply meet_sl_le_spec in E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
IsInjective0: IsInjective f
x, y: L
E: f x ⊓ f y = f x
x ≤ y apply meet_sl_le_spec.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
IsInjective0: IsInjective f
x, y: L
E: f x ⊓ f y = f x
x ⊓ y = x
  rewrite <-preserves_meet in E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
IsInjective0: IsInjective f
x, y: L
E: f (x ⊓ y) = f x
x ⊓ y = x
  apply (injective f).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
f: L -> K
IsMeetPreserving0: IsMeetPreserving f
IsInjective0: IsInjective f
x, y: L
E: f (x ⊓ y) = f x
f (x ⊓ y) = f x assumption.
  Qed.
End meet_order_preserving.

Section order_preserving_join_sl_mor.
  Context `{JoinSemiLatticeOrder L} `{JoinSemiLatticeOrder K}
    `{!TotalOrder (_ : Le L)} `{!TotalOrder (_ : Le K)}
    `{!OrderPreserving (f : L -> K)}.

  Lemma order_preserving_join_sl_mor: IsJoinPreserving f.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
IsJoinPreserving f
  Proof.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
IsJoinPreserving f
  intros x y.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
f (sg_op x y) = sg_op (f x) (f y) case (total (≤) x y); intros E.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: x ≤ y
f (sg_op x y) = sg_op (f x) (f y)
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: y ≤ x
f (sg_op x y) = sg_op (f x) (f y)
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: x ≤ y
f (sg_op x y) = sg_op (f x) (f y) change (f (join x y) = join (f x) (f y)).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: x ≤ y
f (x ⊔ y) = f x ⊔ f y
    rewrite (join_r _ _ E),join_r;trivial.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: x ≤ y
f x ≤ f y
    apply (order_preserving _).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: x ≤ y
x ≤ y trivial.
  -
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: y ≤ x
f (sg_op x y) = sg_op (f x) (f y) change (f (join x y) = join (f x) (f y)).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: y ≤ x
f (x ⊔ y) = f x ⊔ f y
    rewrite 2!join_l; trivial.
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: y ≤ x
f y ≤ f x apply (order_preserving _).
L: Type
Ale: Le L
H: Join L
H0: JoinSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Join K
H2: JoinSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: y ≤ x
y ≤ x trivial.
  Qed.
End order_preserving_join_sl_mor.

Section order_preserving_meet_sl_mor.
  Context `{MeetSemiLatticeOrder L} `{MeetSemiLatticeOrder K}
    `{!TotalOrder (_ : Le L)} `{!TotalOrder (_ : Le K)}
    `{!OrderPreserving (f : L -> K)}.

  Lemma order_preserving_meet_sl_mor: IsSemiGroupPreserving f.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
IsSemiGroupPreserving f
  Proof.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
IsSemiGroupPreserving f
  intros x y.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
f (sg_op x y) = sg_op (f x) (f y) case (total (≤) x y); intros E.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: x ≤ y
f (sg_op x y) = sg_op (f x) (f y)
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: y ≤ x
f (sg_op x y) = sg_op (f x) (f y)
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: x ≤ y
f (sg_op x y) = sg_op (f x) (f y) change (f (meet x y) = meet (f x) (f y)).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: x ≤ y
f (x ⊓ y) = f x ⊓ f y
    rewrite 2!meet_l;trivial.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: x ≤ y
f x ≤ f y
    apply (order_preserving _).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: x ≤ y
x ≤ y trivial.
  -
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: y ≤ x
f (sg_op x y) = sg_op (f x) (f y) change (f (meet x y) = meet (f x) (f y)).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: y ≤ x
f (x ⊓ y) = f x ⊓ f y
    rewrite 2!meet_r; trivial.
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: y ≤ x
f y ≤ f x
    apply (order_preserving _).
L: Type
Ale: Le L
H: Meet L
H0: MeetSemiLatticeOrder Ale
K: Type
Ale0: Le K
H1: Meet K
H2: MeetSemiLatticeOrder Ale0
TotalOrder0: TotalOrder (Ale : Le L)
TotalOrder1: TotalOrder (Ale0 : Le K)
f: L -> K
OrderPreserving0: OrderPreserving (f : L -> K)
x, y: L
E: y ≤ x
y ≤ x trivial.
  Qed.
End order_preserving_meet_sl_mor.

Section strict_ordered_field.

  Generalizable Variables Lle Llt Lmeet Ljoin Lapart.
  Context `{@LatticeOrder L Lle Lmeet Ljoin}.
  Context `{@FullPseudoOrder L Lapart Lle Llt}.

  Lemma join_lt_l_l x y z : z < x -> z < x ⊔ y.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
z < x -> z < x ⊔ y
  Proof.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
z < x -> z < x ⊔ y
    intros ltzx.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltzx: z < x
z < x ⊔ y
    refine (lt_le_trans z x _ _ _); try assumption.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltzx: z < x
x ≤ x ⊔ y
    apply join_ub_l.
  Qed.

  Lemma join_lt_l_r x y z : z < y -> z < x ⊔ y.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
z < y -> z < x ⊔ y
  Proof.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
z < y -> z < x ⊔ y
    intros ltzy.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltzy: z < y
z < x ⊔ y
    refine (lt_le_trans z y _ _ _); try assumption.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltzy: z < y
y ≤ x ⊔ y
    apply join_ub_r.
  Qed.

  Lemma join_lt_r x y z : x < z -> y < z -> x ⊔ y < z.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
x < z -> y < z -> x ⊔ y < z
  Proof.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
x < z -> y < z -> x ⊔ y < z
    intros ltxz ltyz.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
x ⊔ y < z
    set (disj := cotransitive ltxz (x ⊔ y)).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
x ⊔ y < z
    refine (Trunc_rec _ disj); intros [ltxxy|ltxyz].
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
x ⊔ y < z
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxyz: x ⊔ y < z
x ⊔ y < z
    -
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
x ⊔ y < z set (disj' := cotransitive ltyz (x ⊔ y)).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
x ⊔ y < z
      refine (Trunc_rec _ disj'); intros [ltyxy|ltxyz].
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
x ⊔ y < z
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltxyz: x ⊔ y < z
x ⊔ y < z
      +
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
x ⊔ y < z assert (ineqx : x ⊔ y <> x).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
x ⊔ y <> x
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
x ⊔ y < z
        {
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
x ⊔ y <> x
          apply lt_ne_flip; assumption.
        }
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
x ⊔ y < z
        assert (nleyx : ~ (y ≤ x))
          by exact (not_contrapositive (join_l x y) ineqx).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
x ⊔ y < z
        assert (lexy : x ≤ y).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
x ≤ y
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
x ⊔ y < z
        {
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
x ≤ y
          apply le_iff_not_lt_flip.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
~ (y < x)
          intros ltyx.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
ltyx: y < x
Empty
          exact (nleyx (lt_le _ _ _)).
        }
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
x ⊔ y < z
        assert (ineqy : x ⊔ y <> y).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
x ⊔ y <> y
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
ineqy: x ⊔ y <> y
x ⊔ y < z
        {
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
x ⊔ y <> y
          apply lt_ne_flip; assumption.
        }
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
ineqy: x ⊔ y <> y
x ⊔ y < z
        assert (nlexy : ~ (x ≤ y))
          by exact (not_contrapositive (join_r x y) ineqy).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
ineqy: x ⊔ y <> y
nlexy: ~ (x ≤ y)
x ⊔ y < z
        assert (leyx : y ≤ x).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
ineqy: x ⊔ y <> y
nlexy: ~ (x ≤ y)
y ≤ x
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
ineqy: x ⊔ y <> y
nlexy: ~ (x ≤ y)
leyx: y ≤ x
x ⊔ y < z
        {
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
ineqy: x ⊔ y <> y
nlexy: ~ (x ≤ y)
y ≤ x
          apply le_iff_not_lt_flip.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
ineqy: x ⊔ y <> y
nlexy: ~ (x ≤ y)
~ (x < y)
          intros ltxy.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
ineqy: x ⊔ y <> y
nlexy: ~ (x ≤ y)
ltxy: x < y
Empty
          exact (nlexy (lt_le _ _ _)).
        }
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
ineqy: x ⊔ y <> y
nlexy: ~ (x ≤ y)
leyx: y ≤ x
x ⊔ y < z
        assert (eqxy : x = y)
          by exact (antisymmetry _ _ _ lexy leyx).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ y <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
ineqy: x ⊔ y <> y
nlexy: ~ (x ≤ y)
leyx: y ≤ x
eqxy: x = y
x ⊔ y < z
        rewrite <- eqxy in ineqx.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltyxy: y < x ⊔ y
ineqx: x ⊔ x <> x
nleyx: ~ (y ≤ x)
lexy: x ≤ y
ineqy: x ⊔ y <> y
nlexy: ~ (x ≤ y)
leyx: y ≤ x
eqxy: x = y
x ⊔ y < z
        destruct (ineqx (join_idempotent x)).
      +
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxxy: x < x ⊔ y
disj':= cotransitive ltyz (x ⊔ y): hor (y < x ⊔ y) (x ⊔ y < z)
ltxyz: x ⊔ y < z
x ⊔ y < z assumption.
    -
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
ltyz: y < z
disj:= cotransitive ltxz (x ⊔ y): hor (x < x ⊔ y) (x ⊔ y < z)
ltxyz: x ⊔ y < z
x ⊔ y < z assumption.
  Qed.

  Lemma meet_lt_r_l x y z : x < z -> x  ⊓ y < z.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
x < z -> x ⊓ y < z
  Proof.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
x < z -> x ⊓ y < z
    intros ltxz.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
x ⊓ y < z
    refine (le_lt_trans _ x _ _ _); try assumption.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxz: x < z
x ⊓ y ≤ x
    apply meet_lb_l.
  Qed.

  Lemma meet_lt_r_r x y z : y < z -> x  ⊓ y < z.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
y < z -> x ⊓ y < z
  Proof.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
y < z -> x ⊓ y < z
    intros ltyz.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltyz: y < z
x ⊓ y < z
    refine (le_lt_trans _ y _ _ _); try assumption.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltyz: y < z
x ⊓ y ≤ y
    apply meet_lb_r.
  Qed.

  Lemma meet_lt_l x y z : x < y -> x < z -> x < y ⊓ z.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
x < y -> x < z -> x < y ⊓ z
  Proof.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
x < y -> x < z -> x < y ⊓ z
    intros ltxy ltxz.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
x < y ⊓ z
    set (disj := cotransitive ltxy (y ⊓ z)).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
x < y ⊓ z
    refine (Trunc_rec _ disj); intros [ltxyy|ltyzy].
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltxyy: x < y ⊓ z
x < y ⊓ z
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
x < y ⊓ z
    -
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltxyy: x < y ⊓ z
x < y ⊓ z assumption.
    -
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
x < y ⊓ z set (disj' := cotransitive ltxz (y ⊓ z)).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
x < y ⊓ z
      refine (Trunc_rec _ disj'); intros [ltxyz|ltyzz].
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltxyz: x < y ⊓ z
x < y ⊓ z
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
x < y ⊓ z
      +
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltxyz: x < y ⊓ z
x < y ⊓ z assumption.
      +
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
x < y ⊓ z assert (ineqy : y ⊓ z <> y).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
y ⊓ z <> y
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
x < y ⊓ z
        {
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
y ⊓ z <> y
          apply lt_ne; assumption.
        }
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
x < y ⊓ z
        assert (nleyz : ~ (y ≤ z))
          by exact (not_contrapositive (meet_l y z) ineqy).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
x < y ⊓ z
        assert (lezy : z ≤ y).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
z ≤ y
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
x < y ⊓ z
        {
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
z ≤ y
          apply le_iff_not_lt_flip.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
~ (y < z)
          intros ltzy.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
ltzy: y < z
Empty
          exact (nleyz (lt_le _ _ _)).
        }
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
x < y ⊓ z
        assert (ineqz : y ⊓ z <> z).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
y ⊓ z <> z
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
ineqz: y ⊓ z <> z
x < y ⊓ z
        {
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
y ⊓ z <> z
          apply lt_ne; assumption.
        }
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
ineqz: y ⊓ z <> z
x < y ⊓ z
        assert (nlezy : ~ (z ≤ y))
          by exact (not_contrapositive (meet_r y z) ineqz).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
ineqz: y ⊓ z <> z
nlezy: ~ (z ≤ y)
x < y ⊓ z
        assert (leyz : y ≤ z).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
ineqz: y ⊓ z <> z
nlezy: ~ (z ≤ y)
y ≤ z
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
ineqz: y ⊓ z <> z
nlezy: ~ (z ≤ y)
leyz: y ≤ z
x < y ⊓ z
        {
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
ineqz: y ⊓ z <> z
nlezy: ~ (z ≤ y)
y ≤ z
          apply le_iff_not_lt_flip.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
ineqz: y ⊓ z <> z
nlezy: ~ (z ≤ y)
~ (z < y)
          intros ltzy.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
ineqz: y ⊓ z <> z
nlezy: ~ (z ≤ y)
ltzy: z < y
Empty
          exact (nlezy (lt_le _ _ _)).
        }
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
ineqz: y ⊓ z <> z
nlezy: ~ (z ≤ y)
leyz: y ≤ z
x < y ⊓ z
        assert (eqyz : y = z)
          by exact (antisymmetry _ _ _ leyz lezy).
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ z <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
ineqz: y ⊓ z <> z
nlezy: ~ (z ≤ y)
leyz: y ≤ z
eqyz: y = z
x < y ⊓ z
        rewrite <- eqyz in ineqy.
L: Type
Lle: Le L
Lmeet: Meet L
Ljoin: Join L
H: LatticeOrder Lle
Lapart: Apart L
Llt: Lt L
H0: FullPseudoOrder Lle Llt
x, y, z: L
ltxy: x < y
ltxz: x < z
disj:= cotransitive ltxy (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < y)
ltyzy: y ⊓ z < y
disj':= cotransitive ltxz (y ⊓ z): hor (x < y ⊓ z) (y ⊓ z < z)
ltyzz: y ⊓ z < z
ineqy: y ⊓ y <> y
nleyz: ~ (y ≤ z)
lezy: z ≤ y
ineqz: y ⊓ z <> z
nlezy: ~ (z ≤ y)
leyz: y ≤ z
eqyz: y = z
x < y ⊓ z
        destruct (ineqy (meet_idempotent y)).
  Qed.


End strict_ordered_field.