proposition: Lemma pickP : pick_spec (pick P).
proof: Proof. rewrite /pick; case: (enum _) (mem_enum P) => [|x s] Pxs /=. by right; apply: fsym. by left; rewrite -[P _]Pxs mem_head. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)