proposition: Lemma eq_disjoint0 A B : A =i pred0 -> [disjoint A & B].
proof: Proof. by move/eq_disjoint->; apply: disjoint0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)