proposition: Lemma dot_neg_point {Hl: BL+CNV ≪ l} {n m k} {x: X n m} {p: X m k} {Hp: is_point p}: !x ⋅ p ≡ !(x⋅p).
proof: Proof. apply antisym. apply dot_neg_inj. apply dot_neg_surj. Qed.
imports: common lattice monoid kleene normalisation rewriting