proposition: Lemma disjoint_cons x s B : [disjoint x :: s & B] = (x \notin B) && [disjoint s & B].
proof: Proof. exact: disjointU1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)