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