proposition: Lemma dotplsx `{laws} `{CUP ≪ l} n m p (x y: X n m) (z: X m p): (x+y)⋅z ≡ x⋅z+y⋅z.
proof: Proof. apply antisym. 2: apply leq_cupx; apply dot_leq; lattice. destruct dotplsx_ as [Hl|E]. 2: apply E. rewrite <-rdv_spec. apply leq_cupx; rewrite rdv_spec; lattice. Qed.
imports: lattice