proposition: Lemma fpowersetCE (X A B : {fset K}) : (A \in fpowerset (X `\` B)) = (A `<=` X) && [disjoint A & B]%fset.
proof: Proof. by rewrite fpowersetE fsubsetD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)