proposition: Lemma dotx0 `{laws} `{BOT ≪ l} n m p (x: X p m): x⋅0 ≡ zer p n.
proof: Proof. apply antisym. 2: apply leq_bx. destruct dotx0_ as [Hl|[Hl|E]]. rewrite <-ldv_spec. apply leq_bx. cnv_switch. rewrite cnvdot,2cnv0. apply weq_leq, dot0x. apply E. Qed.
imports: lattice