proposition: Lemma leq_pxq `{AL+TOP ≪ l} {n m k} {p: X n k} {q: X m k} {x: X n m} {Hp: is_point p} {Hq: is_point q}: p ≦ x⋅q <-> q ≦x°⋅p.
proof: Proof. rewrite 2leq_xyp. now rewrite cnv_leq_iff', cnvdot, cnv_invol. Qed.
imports: common lattice monoid kleene normalisation rewriting