proposition: Lemma BQdiff_diff a b c: ratp a -> ratp b -> ratp c -> a -q (b -q c) = (a -q b) +q c.
proof: Proof. move => aq bq cq; rewrite /BQdiff (BQoppD bq (QSo cq)) (BQopp_K cq) BQsumA //. by apply:QSo. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)