proposition: Lemma fsetDK A B : B `<=` A -> A `\` (A `\` B) = B.
proof: Proof. by rewrite fsetDDr => /fsetIidPr->; rewrite fsetDv fset0U. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)