Lemma bottom_interlacing_consensus_t {X : hSet} {b : interlaced_prebilattice X} {x y z : X} (p : tle b z x) (q : tle b z y) : tle b z (consensus b x y). Proof. rewrite <- (Lmin_id (klattice b) z). use (double_interlacing_consensus_t 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.