proposition: Lemma pred0Pn P : reflect (exists x, P x) (~~ pred0b P).
proof: Proof. case: (pickP P) => [x Px | P0]. by rewrite (introN (pred0P P)) => [|P0]; [left; exists x | rewrite P0 in Px]. by rewrite -lt0n eq_card0 //; right=> [[x]]; rewrite P0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)