Lemma interlaced_leqt_leqk_leqkmeet {X : hSet} : ∏ (b : interlaced_prebilattice X) (x y : X) , (∑ r : X, tle b x r × kle b r y) -> kle b x (meet b y x). Proof. intros ? x y [? [p1 p2]]. set (w := (meet _ y x)); rewrite <- (Lmin_le_eq_r _ _ _ p1). use (interlacing_meet_k _ _ _ _ p2). 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.