proposition: Lemma BZ_of_Z_injective x y : BZ_of_Z x = BZ_of_Z y -> x = y.
proof: Proof. case: x; case: y; simpl => n m /= eq. - by move:(nat_to_B_injective (BZ_of_nat_inj eq)) => ->. - move: (positive_non_zero1 m) (positive_non_zero2 n); rewrite -eq => pa pb. case: (BZ_di_neg_pos pb pa). - move: (positive_non_zero1 n) (positive_non_zero2 m); rewrite -eq => pa pb. case: (BZ_di_neg_pos pb pa). - have pa: cardinalp (nat_to_B m) by move: (nat_to_B_Nat m) => h; fprops. have pb: cardinalp (nat_to_B n) by move: (nat_to_B_Nat n) => h; fprops. move:(csucc_inj pa pb (BZm_of_nat_inj eq)) => eq2. by rewrite (nat_to_B_injective eq2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)