proposition: Lemma BQsum_cZ x y: intp x -> intp y -> BQ_of_Z x +q BQ_of_Z y = BQ_of_Z (x +z y).
proof: Proof. move => xz yz. move: (BQ_of_Z_iQ xz) (BQ_of_Z_iQ yz) => x'Q y'Q. have h: Q (BQ_of_Z x) = Q (BQ_of_Z y) by rewrite /BQ_of_Z ! pr2_pair. by rewrite BQsum_same_den // /BQ_of_Z ; aw; rewrite - BQ_of_Z_pr0 //; apply:ZSs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)