proposition: Lemma cprod_ntriv A B : A != 1 -> B != 1 -> A \* B = if [&& group_set A, group_set B & B \subset 'C(A)] then A * B else set0.
proof: Proof. move=> A1 B1; rewrite /cprod; case: ifP => cAB; rewrite ?cAB ?andbF //=. by rewrite /pprod -if_neg A1 -if_neg B1 cents_norm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)