proposition: Lemma mem_repr A x : x \in A -> repr A \in A.
proof: Proof. by rewrite /repr; case: ifP => // _; case: pickP => // A0; rewrite [x \in A]A0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)