proposition: Lemma Qdiv_Mltltge2 a b c: ratp a -> inc b BQps -> ratp c -> (a /q b <q c <-> a <q b *q c).
proof: Proof. move => pa pb pc. move:(BQdiv_Mltltge0 pa pb pc QpsS1). by rewrite (BQprod_1r pa) (BQdiv_x1 pc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)