proposition: Lemma BZ_ind (p:property): p \0z -> (forall x, intp x -> p x -> p (BZsucc x)) -> (forall x, intp x -> p x -> p (BZpred x)) -> forall n, inc n BZ -> p n.
proof: Proof. move: ZS0 => pa pb pc pd n nz; apply: (BZ_ind1 pa pb _ _ nz). by move=> x [_ xb _]; apply: pc. by move=> x [xb _ _]; apply: pd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)