proposition: Lemma BQprod_mle2r 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_Mlele0;apply:BQms_sBQm. move => h; case: (qleT_el pa pb) => // h1. move: (BQprod_Mltlt0 pc h1) => h2; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)