proposition: Lemma disjoint_cat s1 s2 A : [disjoint s1 ++ s2 & A] = [disjoint s1 & A] && [disjoint s2 & A].
proof: Proof. by rewrite !disjoint_has has_cat negb_or. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)