proposition: Lemma BZsucc_N x: natp x -> BZsucc (BZ_of_nat x) = BZ_of_nat (csucc x).
proof: Proof. move => xB; rewrite /BZsucc (BZsum_pp (BZ_of_natp_i xB) (BZ_of_natp_i NS1)). by rewrite ! BZ_of_nat_val (Nsucc_rw xB). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)