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