proposition: Lemma BZ_of_Z_sign (x:int): BZ_of_Z (Num.sg x) = BZsign (BZ_of_Z x).
proof: Proof. case: x => /= p. rewrite sgrEz;case: p => /=; first by rewrite BZsign_0. move => p; rewrite (BZsign_pos) ? succ_zero //. apply/BZps_iP; split. apply: BZ_of_natp_i; apply: NS_succ; apply: nat_to_B_Nat. move=> h; move: (f_equal P h); rewrite BZ_of_nat_val BZ0_val;apply: succ_nz. rewrite (BZsign_neg (positive_non_zero2 p)) succ_zero //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)