proposition: Lemma disjoint_vect_iff `{BL+CNV ≪ l} {n m} {p q: X n m} {Hq: is_vector q}: p ⊓ q ≦ 0 <-> q°⋅p ≦ 0.
proof: Proof. rewrite Schroeder_l, cnv_invol, negbot. rewrite vector, capC. apply leq_cap_neg'. Qed.
imports: common lattice monoid kleene normalisation rewriting