proposition: Lemma atom_points `{AL+TOP ≪ l} {n m k} {a: X n m} {Ha: is_atom a} {Hk: is_nonempty' k}: exists p q: X _ k, is_point p /\ is_point q /\ a ≡ p⋅q°.
proof: Proof. exists (a⋅top). exists (a°⋅top). split. rewrite <-top_nnm, dotA. apply gen_point. assumption. apply point_a_top. split. rewrite <-top_nnm, dotA. apply gen_point. assumption. apply point_a'_top. ra_normalise. mrewrite (top_nonempty (n:=m) (p:=n)). now rewrite a_top_a. Qed.
imports: common lattice monoid kleene normalisation rewriting