proposition: Lemma BZprec_N x: inc x Nats -> BZpred (BZ_of_nat x) = BZ_of_nat (cpred x).
proof: Proof. move /setC1_P => [pa pb]; move: (cpred_pr pa pb) => [qa qb]. move: (BZ_of_nat_i qa) => pc. rewrite {1} qb - (BZsucc_N qa) /BZsucc /BZpred /BZdiff. by rewrite - (BZsumA pc ZS1 (ZSo ZS1)) (BZsum_opp_r ZS1) BZsum_0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)