proposition: Lemma BQdiv_le1P a b c: ratp a -> inc b BQps -> inc c BQps -> (a /q b <=q c <-> a /q c <=q b).
proof: Proof. move => aq bp cp. move/BQps_iP: (bp) => [/BQp_sBQ bq bnz]. move/BQps_iP: (cp) => [/BQp_sBQ cq cnz]. move: (BQprod_ple2r (QS_div aq bq) cq bp). rewrite BQprodC (BQprod_div bq aq bnz) => h1. move: (BQprod_ple2r (QS_div aq cq) bq cp). rewrite BQprodC (BQprod_div cq aq cnz) BQprodC => h2. exact: (iff_trans (iff_sym h1) h2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)