Lemma interlaced_geqt_geqk_geqkjoin {X: hSet} : ∏ (b : interlaced_prebilattice X) (x y : X) , (∑ r : X, tle b r x × kle b y r) -> kle b (join b y x) x . Proof. intros b' ? ? [? [p1 p2]]. set (bop := make_interlaced_prebilattice (opp_prebilattice_is_interlaced b')). set (H := interlaced_leqt_leqk_leqkmeet bop _ _ (_,,(Lmax_le_eq_l _ _ _ p1),, (Lmax_le_eq_l _ _ _ p2))). use (Lmax_le_eq_l _ _ _ H). 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.