proposition: Lemma proper1set A x : ([set x] \proper A) -> (x \in A).
proof: Proof. by move/proper_sub; rewrite sub1set. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)