proposition: Lemma BQdiff_diff2 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. by move:(BQdiff_diff aq bq (QSo cq)); rewrite /BQdiff (BQopp_K cq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)