proposition: Lemma BQdiff_sum_simpl_l: (x +q y) -q (x +q z) = y -q z.
proof: Proof. rewrite /BQdiff (BQoppD xq zq) (BQsumC x y). rewrite (BQsumA (QSs yq xq) (QSo xq) (QSo zq)). by rewrite -(BQsumA yq xq (QSo xq)); rewrite BQsum_opp_r // BQsum_0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)