proposition: Lemma fdisjoint1X x A : [disjoint [fset x] & A] = (x \notin A).
proof: Proof. rewrite -(@disjoint_fsub (x |` A)) //. by rewrite (@eq_disjoint1 _ [` fset1U1 _ _]) ?inE =>// ?; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)