proposition: Lemma eq_disjoint A B : A =i B -> disjoint (mem A) =1 disjoint (mem B).
proof: Proof. by move=> eqAB [C]; congr (_ == 0); apply: eq_card => x; rewrite !inE eqAB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)