proposition: Lemma point_lattice_atom {Hl: AL+TOP ≪ l} {n m} {p v: X n m} {Hp: is_point p} {Hv: is_vector v}: is_nonempty v -> v ≦ p -> v ≡ p.
proof: Proof. intros Hv' Hvp. apply antisym. assumption. assert (is_nonempty (p ∩ v)). rewrite leq_iff_cap in Hvp. now rewrite capC, Hvp. apply leq_iff_cap. cnv_switch. ra_normalise. apply univalent_antisym. 2: lattice. cnv_switch. ra_normalise. rewrite (leq_xt (top⋅p)). rewrite nonempty. now rewrite <-dotA, vector. Qed.
imports: common lattice monoid kleene normalisation rewriting