proposition: Lemma disjoint_sym A B : [disjoint A & B] = [disjoint B & A].
proof: Proof. by congr (_ == 0); apply: eq_card => x; apply: andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)