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