proposition: Lemma Schroeder_ `{laws} `{BL+CNV ≪ l} n m p (x : X n m) (y : X m p) (z : X n p): x°⋅!z ≦ !y -> x⋅y ≦ z.
proof: Proof. intro E. apply leq_cap_neg in E. rewrite negneg in E. apply leq_cap_neg. now rewrite capdotx, capC, E, dotx0. Qed.
imports: lattice