proposition: Lemma BZ_of_Z_succ (x:int): BZ_of_Z (1 + x) = \1z +z BZ_of_Z x.
proof: Proof. have cp:forall (n: nat), BZ_of_Z (1 + (Posz n)) = \1z +z BZ_of_Z n. move => n. have pa: cardinalp (nat_to_B n) by move: (nat_to_B_Nat n) => h; fprops. simpl; rewrite (BZsum_pp (BZps_sBZp ZpsS1) (positive_non_zero1 n)). rewrite 2!BZ_of_nat_val csumC csucc_pr4 //. case: x=> // n. rewrite BZ_of_Z_neg NegzE. have ->: Posz(n.+1) = 1 + Posz n by []. have nz := (BZ_of_Z_inc n). rewrite cp (BZoppD ZS1 nz) (BZsumA ZS1 (ZSo ZS1) (ZSo nz)). rewrite (BZsum_opp_r ZS1) (BZsum_0l (ZSo nz)) - BZ_of_Z_opp opprD. by rewrite - {1} (opprK 1) addKr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)