proposition: Lemma cprodC : commutative cprod.
proof: Proof. rewrite /cprod => A B; case: ifP => cAB; rewrite centsC cAB // /pprod. by rewrite andbCA normC !cents_norm // 1?centsC //; do 2!case: eqP => // ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)