proposition: Lemma cfclass_uniq phi : H <| G -> uniq (phi ^: G)%CF.
proof: Proof. move=> nsHG; rewrite map_inj_in_uniq ?enum_uniq // => Ty Tz; rewrite !mem_enum. move=> {Ty}/rcosetsP[y Gy ->] {Tz}/rcosetsP[z Gz ->] /eqP. case: repr_rcosetP => u Iphi_u; case: repr_rcosetP => v Iphi_v. have [[Gu _] [Gv _]] := (setIdP Iphi_u, setIdP Iphi_v). rewrite cfConjg_eqE ?groupM // => /rcoset_eqP. by rewrite !rcosetM (rcoset_id Iphi_v) (rcoset_id Iphi_u). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop prime order) mathcomp(ssralg ssrnum finset fingroup morphism perm) mathcomp(automorphism quotient action zmodp cyclic center) mathcomp(gproduct commutator gseries nilpotent pgroup) mathcomp(sylow maximal frobenius matrix mxalgebra) mathcomp(mxrepresentation vector algC classfun character) mathcomp(archimedean)