proposition: Lemma BQdiv_Mle1 a b c: ratp a -> ratp b -> inc c BQps -> ( a <=q b *q c <-> a /q c <=q b).
proof: Proof. move => aq bq cqp; move:(QpsS_inv cqp) => ip. move/BQps_iP: (cqp) => [/BQp_sBQ cp cnz]. split => h. move: (BQprod_Mlege0 (BQps_sBQp ip) h). rewrite (BQprodC b) -! /(BQdiv _ _) BQdiv_prod //. move: (BQprod_Mlege0 (BQps_sBQp cqp) h). rewrite BQprodC BQprod_div //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)