proposition: Lemma simple_neg : simple -> forall v w, g v w -> v != w.
proof: Proof. move=> H v w; apply: contraTN => /eqP ->; by apply H. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext