proposition: Fact nat_hasChoice : hasChoice nat.
proof: Proof. pose f := [fun (P : pred nat) n => if P n then Some n else None]. exists f => [P n m | P [n Pn] | P Q eqPQ n] /=; last by rewrite eqPQ. by case: ifP => // Pn [<-]. by exists n; rewrite Pn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)