proposition: Lemma in_setD A B x : (x \in A :\: B) = (x \notin B) && (x \in A).
proof: Proof. exact: in_set. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)