proposition: Lemma BQfloor_M x y: x <=q y -> BQfloor x <=z BQfloor y.
proof: Proof. move => h; move:(h) => [xq yq _]. move: ( BQ_floorp xq)( BQ_floorp yq) => [sa _][_ sd]. move: (ZS_floor xq) => fxz. move: (ZS_floor yq) => fyz. move: (qle_ltT (qleT sa h) sd); rewrite (BQsum_cZ fyz ZS1). by move / (qlt_cZ fxz (ZSs fyz ZS1)) => /(zlt_succ1P fxz fyz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)