proposition: Lemma BZprodC x y: x *z y = y *z x.
proof: Proof. rewrite BZprodE /BZprod_int cprodC. case: (equal_or_not (Q x) (Q y)); first by move => ->. by move => h; move: (nesym h) => h1; Ytac0; Ytac0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)