proposition: Lemma fmvalJcond u x : val (u ^@ x) = if x \in 'N(A) then val u ^ x else val u.
proof: Proof. by case: ifP => Nx; rewrite /actr Nx ?fmodK // memJ_norm ?fmodP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype bigop ssralg finset fingroup) mathcomp(morphism perm finalg action gproduct commutator) mathcomp(cyclic)