proposition: Lemma BZ_ind1 a (p:property): intp a -> p a -> (forall x, BZ_le a x -> p x -> p (BZsucc x)) -> (forall x, BZ_le x a -> p x -> p (BZpred x)) -> forall n, inc n BZ -> p n.
proof: Proof. move => az pa pb pc n nz; case: (zleT_ee az nz). by apply:BZ_induction_pos. by apply:BZ_induction_neg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)