proposition: Lemma BZ_succ_pred (r := BZ_order) x: intp x -> [/\ consecutive r x (BZsucc x), consecutive r (BZpred x) x, or_succ r x = BZsucc x & or_pred r x = BZpred x].
proof: Proof. move => xz. have pa: consecutive r x (BZsucc x). split; first by apply /zlt_P; apply: zlt_succ. rewrite BZor_sr => z zz [/zlt_P ha /zlt_P /(zlt_succ1P zz xz) hb]; BZo_tac. have pb: consecutive r (BZpred x) x. split; first by apply/zlt_P; apply /zlt_pred. rewrite BZor_sr => z zz [/zlt_P ha /zlt_P hb]. move/(zlt_succ2P (ZS_pred xz) zz):ha;rewrite (BZsucc_pred xz) => hc; BZo_tac. move: (BZor_tor) => tor. split => //. symmetry; apply: (or_succ_prop' tor pa). symmetry; apply: (or_pred_prop' tor pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)