proposition: Lemma mem_fsetD1 a A : a \notin A -> A `\ a = A.
proof: Proof. move=> aA; apply/fsetP => x; rewrite !inE andbC. by have [/= xA|//] := boolP (_ \in A); apply: contraNneq aA => <-. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)