proposition: Lemma colorable_is_simple n (coloring : V -> 'I_n) : colorable g coloring -> simple.
proof: Proof. by move=> H v; apply H. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext