proposition: Lemma point_a_top `{CNV+TOP ≪ l} {n m} {a: X n m} {Ha: is_atom a}: is_point (a⋅top' m m).
proof: Proof. split. unfold is_vector. now mrewrite top_nnm. unfold is_injective. ra_normalise. mrewrite top_nnm. apply a_top_a'. intros i j. mrewrite top_nnm. apply atom_nonempty. Qed.
imports: common lattice monoid kleene normalisation rewriting