proposition: Lemma fsubsetDP A B C : reflect (A `<=` B /\ [disjoint A & C]%fset) (A `<=` (B `\` C)).
proof: Proof. by rewrite fsubsetD; apply: andP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)