proposition: Lemma qle_diffP a b: ratp a -> ratp b -> (a <=q b <-> inc (b -q a) BQp).
proof: Proof. move => aq bq. move /BQ_P: (aq) => [_ pa pb _]; move: (BZps_sBZ pb) => pc. move /BQ_P: (bq) => [_ qa qb _]; move: (BZps_sBZ qb) => qc. rewrite /BQdiff /BQsum /BQopp pr1_pair pr2_pair. set x := (P b *z Q a +z Q b *z BZopp (P a)). have aux: P a *z Q b <=z Q a *z P b <-> inc x BZp. rewrite /x (BZprodC (P b)) -(BZopp_prod_r qc pa) (BZprodC (Q b)). exact: (zle_diffP (ZSp pa qc) (ZSp pc qa)). move: (ZpsS_prod qb pb) => dp. split; first by move => [_ _ /aux h]; apply:(BQ_of_pair_pos h dp). move => h; split => //; apply/aux. have: intp x by apply:ZSs; apply:ZSp => //; apply: ZSo. case/BZ_i0P => // h2. by case:(BQ_di_neg_pos(BQ_of_pair_sneg h2 (ZpsS_prod qb pb)) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)