proposition: Lemma fsetDidPl A B : reflect (A `\` B = A) [disjoint A & B]%fset.
proof: Proof. apply: (iffP fdisjointP)=> [NB|<- a]; last by rewrite inE => /andP[]. apply/fsetP => a; rewrite !inE andbC. by case: (boolP (a \in A)) => //= /NB ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)