proposition: Lemma in_fsetD A B a : (a \in A `\` B) = (a \notin B) && (a \in A).
proof: Proof. by rewrite in_fset andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)