proposition: Lemma sub1set A x : ([set x] \subset A) = (x \in A).
proof: Proof. by rewrite -subset_pred1; apply: eq_subset=> y; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)