proposition: Lemma capcup_ `{laws} `{DL ≪ l}: forall x y z, x ⊓ (y ⊔ z) ≦ (x ⊓ y) ⊔ (x ⊓ z).
proof: Proof. intros. rewrite <- cupcap_. apply leq_xcap. lattice. transitivity (z ⊔ x ⊓ y). 2: lattice. rewrite <- cupcap_. lattice. Qed.
imports: common level