proposition: Lemma atom_of_points `{AL+TOP ≪ l} {n m k} {p: X n m} {q: X k m} {Hp: is_point p} {Hq: is_point q}: is_atom (p⋅q°).
proof: Proof. split. ra_normalise. apply atom_of_points_aux. ra_normalise. apply atom_of_points_aux. intros i j. mrewrite (surjective_tx (x:=p)). now apply nonempty_cnv. Qed.
imports: common lattice monoid kleene normalisation rewriting