proposition: Lemma dedekind `{laws} `{AL ≪ l} n m p (x : X n m) (y : X m p) (z : X n p): x⋅y ⊓ z ≦ (x ⊓ (z⋅y°))⋅(y ⊓ (x°⋅z)).
proof: Proof. rewrite <-(capI z) at 1. rewrite capA, capdotx, capxdot. ra. Qed.
imports: common lattice monoid kleene normalisation rewriting