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