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