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