proposition: Lemma fsetI1 a A : A `&` [fset a] = if a \in A then [fset a] else fset0.
proof: Proof. apply/fsetP => x; rewrite (fun_if (fun X => _ \in X)) !inE. by have [[->|?] []] := (altP (x =P a), boolP (a \in A)); rewrite ?andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)