proposition: Lemma disjoint_has s A : [disjoint s & A] = ~~ has [in A] s.
proof: Proof. apply/negbRL; apply/pred0Pn/hasP => [[x /andP[]]|[x]]; exists x => //. exact/andP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)