proposition: Lemma BZ_order_sfinc f r' (r:= BZ_order) : function_prop f BZ (substrate r') -> order r' -> (forall z, intp z -> glt r' (Vf f z) (Vf f (BZsucc z))) -> strict_increasing_fun f r r'.
proof: Proof. move => pa pd pe. move: BZor_sr (proj1 BZor_tor) => e1 or; rewrite - e1 in pa. split => // x y /zlt_P ltxy. have xz: intp x by BZo_tac. have yz: intp y by BZo_tac. move: y yz ltxy; apply: (BZ_ind1 xz);first by move => []. move => t ta HR _; move: (pe _ (proj32 ta)) => tb. case: (equal_or_not x t) => ext; first by rewrite ext. move: (HR (conj ta ext)) => tc; order_tac. move => t ta _ tb; move: (zlt_leT tb (proj1 (zlt_pred (proj31 ta)))) => za. BZo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)