proposition: Lemma Qdiv_Mlelege1 a c d: ratp a -> ratp c -> inc d BQps -> (a <=q c /q d <-> a *q d <=q c).
proof: Proof. move => pa pc pd. move:(BQdiv_Mlelege0 pa QpsS1 pc pd). by rewrite (BQprod_1l pc) (BQdiv_x1 pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)