proposition: Lemma disjoint_vect_ext {Hl: BL+CNV ≪ l} {n m k} {x y: X n m} {x' y': X m k} {Hx: is_vector x}: x ⊓ y ≦ 0 -> (x ⋅ x') ⊓ (y ⋅ y') ≦ 0.
proof: Proof. rewrite capC. intro H. apply disjoint_vect_iff in H. rewrite capdotx. mrewrite H. ra. Qed.
imports: common lattice monoid kleene normalisation rewriting