proposition: Lemma zlt_succ2P a b: intp a -> intp b -> (BZsucc a <=z b <-> a <z b).
proof: Proof. move => az bz. have H := (zlt_succ1P (ZS_succ az) bz). have Ha := zlt_diffP az bz. have Hb := (zlt_diffP (ZS_succ az) (ZS_succ bz)). have eq:= (BZdiff_sum_simpl_r bz az ZS1). split. by move/H /Hb; rewrite eq => /Ha. by move /Ha; rewrite - eq => /Hb /H. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)