proposition: Lemma BQdiff_cZ x y: intp x -> intp y -> BQ_of_Z x -q BQ_of_Z y = BQ_of_Z (x -z y).
proof: Proof. by move => za /ZSo zb; rewrite /BQdiff (BQopp_cZ y) (BQsum_cZ za zb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)