Proposition distributive_prebilattices_are_interlaced_prebilattices {X : hSet} (b : distributive_prebilattice X) : is_interlaced b . Proof. do 3 (try split); intros x y z H. - rewrite (iscomm_consensus _ x z), (iscomm_consensus _ y z). set(d := ldistr_meet_consensus b x y z). unfold meet in d. cbn. rewrite <- d, H. reflexivity. - rewrite (iscomm_gullibility _ x z), (iscomm_gullibility _ y z). set (d := ldistr_meet_gullibility b x y z). unfold meet in d. cbn. rewrite <- d, H; reflexivity. - rewrite (iscomm_meet _ x z), (iscomm_meet _ y z). set (d := (ldistr_consensus_meet b x y z)). unfold consensus in d. cbn. rewrite <- d , H; reflexivity. - rewrite (iscomm_join _ x z), (iscomm_join _ y z). set (d := ldistr_consensus_join b x y z). unfold consensus in d. cbn. rewrite <- d, H; reflexivity . Defined.
Require Import UniMath.OrderTheory.Prebilattice.Prebilattice. Require Import UniMath.OrderTheory.Prebilattice.Interlaced. Require Import UniMath.Foundations.Sets. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Distributive.