proposition: Lemma pickP h : def h && ~~ empb h = (pick h \in dom h).
proof: Proof. by rewrite /dom; case: h=>[|h] //=; case: (supp h)=>// *; rewrite inE eq_refl. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep