proposition: Lemma BQsum_opp_rev a b: ratp a -> ratp b -> a +q b = \0q -> a = BQopp b.
proof: Proof. move => aq bq h. move: (BQsumA aq bq (QSo bq)). by rewrite (BQsum_opp_r bq) h (BQsum_0l (QSo bq)) (BQsum_0r aq). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)