proposition: Lemma BQprod_mlt2r a b c: ratp a -> ratp b -> inc c BQms -> ((b *q c) <q (a *q c) <-> a <q b).
proof: Proof. move => pa pb pc; split; last by apply:BQprod_Mltlt0. move => h; case: (qleT_el pb pa) => //. move /(BQprod_mle2r pb pa pc) => h2; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)