proposition: Lemma fsub1set A x : ([fset x] `<=` A) = (x \in A).
proof: Proof. rewrite -(@subset_fsubE (x |` A)) // fsub1 ?fset1U1 // => xxA. by rewrite sub1set inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)