proposition: Lemma atom_mono `{AL+TOP ≪ l} {n} {a: X n n} {Ha: is_atom a}: a⋅a ≦ 1.
proof: Proof. transitivity (a⋅a ⊓ a). apply leq_xcap. reflexivity. apply atom_transitive. rewrite dedekind. transitivity ((a⋅a°)⋅(a°⋅a)). apply dot_leq; lattice. mrewrite (injective (x:=a)). mrewrite (univalent (x:=a)). ra. Qed.
imports: common lattice monoid kleene normalisation rewriting