Lemma top_interlacing_join_k {X : hSet} {b : interlaced_prebilattice X} {x y z : X} (p : kle b x z) (q : kle b y z) : kle b (join b x y) z. Proof. rewrite <- (Lmax_id (tlattice b) z). use (double_interlacing_join_k p q). Defined.
Require Import UniMath.OrderTheory.Prebilattice.Prebilattice. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.Algebra.BinaryOperations.