proposition: Lemma cfun_onP A phi : reflect (forall x, x \notin A -> phi x = 0) (phi \in 'CF(G, A)).
proof: Proof. apply: (iffP idP) => [/coord_span-> x notAx | Aphi]. set b := cfun_base G A; rewrite sum_cfunE big1 // => i _; rewrite cfunE. have /mapP[xG]: b`_i \in b by rewrite -tnth_nth mem_tnth. rewrite mem_enum => /setIdP[/imsetP[y Gy ->] Ay] ->. by rewrite cfun_classE Gy (contraNF (subsetP Ay x)) ?mulr0. suffices <-: \sum_(xG in classes G) phi (repr xG) *: '1_xG = phi. apply: memv_suml => _ /imsetP[x Gx ->]; rewrite rpredZeq cfun_repr. have [s_xG_A | /subsetPn[_ /imsetP[y Gy ->]]] := boolP (x ^: G \subset A). by rewrite cfun_on_sum [_ \in _](sumv_sup (x ^: G)) ?mem_classes ?orbT. by move/Aphi; rewrite cfunJ // => ->; rewrite eqxx. apply/cfun_inP=> x Gx; rewrite sum_cfunE (bigD1 (x ^: G)) ?mem_classes //=. rewrite cfunE cfun_repr cfun_classE Gx class_refl mulr1. rewrite big1 ?addr0 // => _ /andP[/imsetP[y Gy ->]]; apply: contraNeq. rewrite cfunE cfun_repr cfun_classE Gy mulf_eq0 => /norP[_]. by rewrite pnatr_eq0 -lt0n lt0b => /class_eqP->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)