proposition: Lemma a_top_a_aux `{AL+TOP ≪ l} {n m} {a: X n m} {Ha: is_atom a}: (a ⋅ top) ∩ (top ⋅ a) ≡ a.
proof: Proof. apply antisym. rewrite capdotx. mrewrite a'_top_a. ra. rewrite <-2(leq_xt 1). ra. Qed.
imports: common lattice monoid kleene normalisation rewriting