proposition: Lemma BZ_of_Zp_surjective x : inc x BZp -> exists y:nat, BZ_of_Z y = x.
proof: Proof. move => pa. rewrite - (BZp_hi_pr pa). move /indexed_P: pa => [_ pc _]. move: (nat_to_B_surjective pc) => [n ->]; by exists n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)