proposition: Lemma triv_sign_neq n : (n > 1)%N -> 1 != sign_char :> 'CF('SG_n).
proof: Proof. case: n => // n; rewrite ltnS => Hn. apply/negP=> /eqP/cfunP /(_ 's_0)/eqP. rewrite cfunE cfun1E inE /= (odd_eltr Hn) /= expr1 -addr_eq0 -mulr2n. by have := Cchar; rewrite charf0P => /(_ 2) ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(fingroup perm ssralg morphism perm action) mathcomp(zmodp) mathcomp(vector matrix mxalgebra ssrnum algC) mathcomp(mxrepresentation classfun character) permcomp tools partition congr cycles cycletype presentSn