proposition: Lemma fdisjointP {A B} : reflect (forall a, a \in A -> a \notin B) [disjoint A & B]%fset.
proof: Proof. apply: (iffP eqP) => [AIB_eq0 a aA|neq_ab]. by have /fsetP /(_ a) := AIB_eq0; rewrite !inE aA /= => ->. apply/fsetP => a; rewrite !inE. by case: (boolP (a \in A)) => // /neq_ab /negPf ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)