proposition: Lemma pred0P P : reflect (P =1 pred0) (pred0b P).
proof: Proof. by apply: (iffP eqP); [apply: card0_eq | apply: eq_card0]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)