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