proposition: Lemma BRprod_auxC x y: (BRprod_aux x y) = (BRprod_aux y x).
proof: Proof. by set_extens a => /BR_prod_auxP [z zx [t ty ->]]; apply/BR_prod_auxP; ex_tac; ex_tac; rewrite BQprodC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)