proposition: Lemma BQoppD x y: ratp x -> ratp y -> BQopp (x +q y) = (BQopp x) +q (BQopp y).
proof: Proof. move => xq yq. move: (QSo xq)(QSo yq) => oxq oyq. symmetry; apply: BQsum_opp_rev; try apply:QSs => //. rewrite BQsum_ACA // (BQsumC _ y) (BQsum_opp_r yq). by rewrite (BQsumC _ x) (BQsum_opp_r xq)(BQsum_0l QS0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)