proposition: Lemma eq_disjoint_r A B : A =i B -> (@disjoint T)^~ (mem A) =1 (@disjoint T)^~ (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)