proposition: Lemma qlt_diffP3 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: (qlt_diffP1 (QSs aq cq) bq). rewrite BQsumC (BQdiff_diff2 bq cq aq). apply: (iff_trans (iff_sym (qlt_diffP1 aq (QS_diff bq cq)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)