proposition: Lemma BQsumC x y: x +q y = y +q x.
proof: Proof. rewrite /BQsum /BQ_of_pair. rewrite (BZprodC (Q x) (Q y)) (BZprodC (P x) (Q y)) (BZprodC (Q x) (P y)). by rewrite (BZsumC ( Q y *z P x)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)