proposition: Lemma BZ_of_Z_sum (x y: int): BZ_of_Z (x + y) = (BZ_of_Z x) +z (BZ_of_Z y).
proof: Proof. move: x y; apply: int_rec. move => y; rewrite add0r /= BZsum_0l //; apply:BZ_of_Z_inc. move => n Hrec y. have ->: BZ_of_Z n.+1 = (BZ_of_Z n) +z \1z by rewrite BZsumC - BZ_of_Z_succ. have ->: (Posz(n.+1) + y) = 1 + (Posz n + y) by rewrite addrA; congr (_ + _). have z1 := ZS1. rewrite BZ_of_Z_succ (BZsumC _ \1z). rewrite - BZsumA ? Hrec //; apply: BZ_of_Z_inc. move => n Hrec y. have nz := (BZ_of_Z_inc n). have ynz := (BZ_of_Z_inc (y-1)). rewrite addrC - opprB (BZ_of_Z_opp n.+1). have ->: (Posz(n.+1) - y) = 1 + (Posz n - y) by rewrite addrA; congr (_ + _). have ->: Posz(n.+1) = 1 + Posz n by []. have aux : y = 1 + (y - 1) by rewrite addrC (subrK 1 y). rewrite opprD opprB addrC (addrC y) - addrA Hrec. rewrite {2} aux BZ_of_Z_opp 2! BZ_of_Z_succ (BZoppD ZS1 nz). rewrite (BZsum_ACA (ZSo ZS1) (ZSo nz) ZS1 ynz). rewrite (BZsum_opp_l ZS1) BZsum_0l //; apply: (ZSs (ZSo nz) ynz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype order) mathcomp(ssrnat ssrint ssralg ssrnum div)