proposition: Lemma repr_set0 : repr set0 = 1.
proof: Proof. by rewrite /repr; case: pickP => [x|_] /[!inE]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)