proposition: Lemma symmetric_except x : symmetric g -> symmetric (except x).
proof: Proof. by move=> sg ? ?; rewrite exceptE /= sg andbA andbAC -andbA. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext