proposition: Lemma leq_xyp `{AL+TOP ≪ l} {n m k} {p: X m k} {x: X n k} {y: X n m} {Hp: is_point p}: x ≦ y⋅p <-> x⋅p° ≦ y.
proof: Proof. split; intro E. rewrite <-(dotx1 y). rewrite <-injective. now mrewrite <-E. rewrite <-(dotx1 x). rewrite surjective. now mrewrite E. Qed.
imports: common lattice monoid kleene normalisation rewriting