proposition: Lemma BZdvds_monotone a b: inc b BZps -> a %|z b -> a <=z b.
proof: Proof. move => /BZps_iP [bzp bnz] dvd; move: (dvd) => [_ az _]. case /BZ_i0P: az => ap. move:(BZms_sBZ ap)(BZp_sBZ bzp) => az bz. split => //; constructor 2. by rewrite /int_np /int_pp (BZp_sg bzp) (BZms_sg ap). move: (BZdvds_pr dvd) => eq. rewrite eq; apply: (BZprod_Mpp ap). apply /BZps_iP;split => //; first by apply : (ZpS_quo bzp ap). by dneg h; rewrite eq h BZprod_0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)