proposition: Lemma BQdiff_le1P a b c: ratp a -> ratp b -> ratp c -> (a -q b <=q c <-> a -q c <=q b).
proof: Proof. move => aq bq cq. move: (BQsum_le2r (QS_diff aq bq) cq bq). rewrite (BQsum_diff1 bq aq) => ha. move: (BQsum_le2r (QS_diff aq cq) bq cq). rewrite (BQsum_diff1 cq aq) BQsumC => hb. exact: (iff_trans (iff_sym ha) hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)