proposition: Lemma BQsum_opp_r x: ratp x -> x +q (BQopp x) = \0q.
proof: Proof. move => xq. move /BQ_P:(xq) => [_ nx dx _ ]. rewrite (BQsum_same_den xq (QSo xq) (esym (BQopp_den x))) /BQopp pr1_pair. by rewrite BZsum_opp_r // BQnum0_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)