proposition: Lemma disjointW A B C D : A \subset B -> C \subset D -> [disjoint B & D] -> [disjoint A & C].
proof: Proof. by move=> subAB subCD BD; apply/(disjointWl subAB)/(disjointWr subCD). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)