proposition: Lemma BZsucc_disc: x <> BZsucc x.
proof: Proof. move: ZS1 => pb pc. move:(BZdiff_sum xz pb); rewrite - /(BZsucc x) - pc (BZdiff_diag xz) => h. by case: BZ1_nz; rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)