proposition: Lemma BQdiv_Mltltge0 a b c d: ratp a -> inc b BQps -> ratp c -> inc d BQps -> ( a /q b <q c /q d <-> a *q d <q b *q c).
proof: Proof. move => aq bqps cq dqps. move/ BQps_iP: (dqps) => [/BQp_sBQ dq dnz]. move/ BQps_iP: (bqps) => [/BQp_sBQ bq bnz]. have qq: ratp (BQinv d) by apply: QS_inv. split; move => [sa sb];split. + by apply/(BQdiv_Mlelege0 aq bqps cq dqps). + dneg h; move: (f_equal (fun z => z /q d) h). rewrite BQprodC (BQdiv_prod dq aq dnz) => h1. rewrite (f_equal (fun z => z /q b) h1). by rewrite {2} /BQdiv - BQprodA // BQdiv_prod //; apply:QSp. + by apply/(BQdiv_Mlelege0 aq bqps cq dqps). + dneg h; move: (f_equal (fun z => z *q b) h). rewrite BQprodC BQprod_div // => ->. rewrite /BQdiv (BQprodC c)- (BQprodA qq cq bq) (BQprodC (BQinv d)). by rewrite BQprodC ( BQprodC b); apply: BQprod_div => //; apply:QSp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)