proposition: Lemma BZ_order_props: or_likeZ BZ_order.
proof: Proof. move: BZor_tor => tor; split => //. move => x; rewrite BZor_sr; move /BZ_succ_pred => [sa sb _ _]. by split; [ exists (BZsucc x) | exists (BZpred x)]. move => E; rewrite BZor_sr => EZ hE; case: (emptyset_dichot E) => xe; fprops. right; apply: extensionality => //. move: xe => [x xE]. apply: (BZ_ind1 (EZ _ xE) (p := fun t => inc t E) xE) => t ta tE. by move: (hE t tE) =>[ya yb]; move:(BZ_succ_pred (EZ _ tE)) => [_ _ <- _]. by move: (hE t tE) =>[ya yb]; move:(BZ_succ_pred (EZ _ tE)) => [_ _ _ <-]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)