proposition: Lemma qlt_diffP4 a b c: ratp a -> ratp b -> ratp c -> (b -q c <q a <-> b <q a +q c).
proof: Proof. move => aq bq cq. move:(qlt_diffP1 (QS_diff bq cq) aq). rewrite(BQdiff_diff aq bq cq) (BQsum_AC aq (QSo bq) cq) => ha. exact: (iff_trans (iff_sym ha) (qlt_diffP1 bq (QSs aq cq))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)