proposition: Lemma atom_lattice_atom {Hl: AL+TOP ≪ l} {n m} {a x: X n m} {Ha: is_atom a}: is_nonempty x -> x ≦ a -> x ≡ a.
proof: Proof. intros Hx Hax. pose proof point_a_top as Hat. assert(Hxt: is_vector (x ⋅ top' m m)). unfold is_vector. now mrewrite top_nnm. apply univalent_antisym. apply weq_geq. apply point_lattice_atom. intros i j. mrewrite top_nnm. apply nonempty. now rewrite Hax. assumption. Qed.
imports: common lattice monoid kleene normalisation rewriting