proposition: Lemma dot_mono `{AL ≪ l} n (x y: X n n): x ≦ 1 -> y ≦ 1 -> x⋅y ≡ x ⊓ y.
proof: Proof. intros Hx Hy. apply antisym. apply leq_xcap. rewrite Hy; ra. rewrite Hx; ra. transitivity (x⋅1 ⊓ y). ra. rewrite capdotx. rewrite Hx at 2. ra_normalise. apply dot_leq; lattice. Qed.
imports: common lattice monoid kleene normalisation rewriting