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