proposition: Lemma in_fsetP A x : in_fset_spec A x x (x \in A).
proof: Proof. have [xA|xNA] := boolP (x \in A); last by constructor. by have {2}-> : x = val [` xA] by []; constructor. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)