proposition: Lemma BZ_of_Z_surjective x : intp x -> exists y, BZ_of_Z y = x.
proof: Proof. case /BZ_i0P => pa. move: (BZms_hi_pr pa) => [_ <- ]. move /indexed_P: pa => [_ pc _]; move/setC1_P: pc => [pB pnz]. move: (cpred_pr pB pnz) => []; set c := cpred _ => ca ->. by move: (nat_to_B_surjective ca) => [n ->];exists (Negz n). by move/ BZ_of_Zp_surjective: pa => [y ya]; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)