proposition: Lemma zlt_succ1P a b: intp a -> intp b -> (a <z (BZsucc b) <-> a <=z b).
proof: Proof. move => az bz. apply:(iff_trans (zlt_diffP az (ZS_succ bz))). apply: iff_sym; apply: (iff_trans (zle_diffP az bz)). rewrite - (BZdiff_succ_l bz az); split => h. apply:(ZpsS_sum_r h ZpsS1). have ha:= (BZp_hi_pr (BZps_sBZp h)). move: (ZS_diff bz az) => cz; move:(BZpred_succ cz) => pc1. move: h => /indexed_P [_ pc _]. move: (BZprec_N pc); rewrite ha pc1 => ->; apply: BZ_of_natp_i. by move /setC1_P:pc => [pd pe]; move: (cpred_pr pd pe) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)