proposition: Lemma BQdiv_Mlelege0 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: (bqps) => [/BQp_sBQ bq bnz]. move/ BQps_iP: (dqps) => [/BQp_sBQ dq dnz]. have idq :=QS_inv dq. have pb:=QSp cq bq. have pa:=QSp pb idq. move:(BQprod_ple2r (QS_div aq bq) (QS_div cq dq) bqps). rewrite BQprodC (BQprod_div bq aq bnz) BQprodC (BQprodA bq cq idq) (BQprodC b). move:(BQprod_ple2r aq pa dqps). rewrite -/(_ /q d) (BQprodC ((c *q b) /q d)) (BQprod_div dq pb dnz). move => sa sb; exact:(iff_sym(iff_trans sa sb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)