Definition double_interlacing {X : hSet} {op : binop X} {R : hrel X} (i : interlacing op R) (a : istrans R) (c : iscomm op) {x y z w : X} (p : R x y) (q : R z w) : R (op x z) (op y w). Proof. use (a (op x z) (op y z)). - use i. exact p. - rewrite (c y z), (c y w). use i . exact 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.