proposition: Lemma BZpred_succ: BZpred (BZsucc x) = x.
proof: Proof. move: (ZSo ZS1) ZS1 => ha hb. by rewrite /BZsucc /BZpred /BZdiff - BZsumA // BZsum_opp_r // BZsum_0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)