proposition: Lemma cfDprod_eq1 phi psi : phi \is a character -> psi \is a character -> (cfDprod KxH phi psi == 1) = (phi == 1) && (psi == 1).
proof: Proof. move=> /Cnat_char1 Nphi /Cnat_char1 Npsi. apply/eqP/andP=> [phi_psi_1 | [/eqP-> /eqP->]]; last by rewrite cfDprod_cfun1. have /andP[/eqP phi1 /eqP psi1]: (phi 1%g == 1) && (psi 1%g == 1). by rewrite -natr_mul_eq1 // -(cfDprod1 KxH) phi_psi_1 cfun11. rewrite -[phi](cfDprodKl KxH psi1) -{2}[psi](cfDprodKr KxH phi1) phi_psi_1. by rewrite !rmorph1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)