proposition: Lemma zlt_pred1P a b: intp a -> intp b -> (a <z b) <-> a <=z (BZpred b).
proof: Proof. by move => az bz; move: (zlt_succ1P az (ZS_pred bz)); rewrite BZsucc_pred. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)