proposition: Lemma disjoint1 x A : [disjoint pred1 x & A] = (x \notin A).
proof: Proof. apply/negbRL/(sameP (pred0Pn _))=> /=. apply: introP => [Ax | notAx [_ /andP[/eqP->]]]; last exact: negP. by exists x; rewrite inE eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)