proposition: Lemma BQ_floor_zero a b: inc a BQp -> a <q b -> BQfloor (a/q b) = \0z.
proof: Proof. move => ap cab. have aq := (BQp_sBQ ap). have bqps: inc b BQps by apply/ qlt0xP; apply: qle_ltT cab; apply/ qle0xP. have pa: inc (a /q b) BQp by apply:(QpS_div ap (BQps_sBQp bqps)). have pb: BQ_of_Z \0z <=q a /q b by apply / qle0xP. have pc: a /q b <q BQ_of_Z \0z +q \1q. rewrite (BQsum_0l QS1). by apply/(BQdiv_lt1P aq QpsS1 bqps); rewrite (BQdiv_x1 aq). symmetry; apply: (BQ_floorp2 (proj32 pb) ZS0 (conj pb pc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)