proposition: Lemma atom_of_points_aux `{AL+TOP ≪ l} {n m k} {p: X n m} {q: X k m} {Hp: is_point p} {Hq: is_point q}: p ⋅ q° ⋅ top ⋅ q ⋅ p° ≦ 1.
proof: Proof. mrewrite surjective_tx. transitivity (p⋅(top⋅q)°⋅p°). ra. mrewrite surjective_tx. ra_normalise. rewrite vector. now apply injective. Qed.
imports: common lattice monoid kleene normalisation rewriting