proposition: Lemma colorable_path_kind n (kind : V -> 'I_n) : colorable kind -> forall t h, path g h t -> forall i h0, i < size t -> kind (nth h0 (h :: t) i) != kind (nth h0 (h :: t) i.+1).
proof: Proof. move=> Hcol; elim => // h [_ h0 /andP[h0h _] i h1|h1 t IH h0]. rewrite ltnS leqn0 => /eqP -> /=; apply/eqP => /Hcol; by rewrite h0h. rewrite [h1 :: t]lock /= -lock => /andP[eh0h hh1t] [|[/= _ _|i h0']]. move=> /= _ _; apply/eqP => /Hcol; by rewrite eh0h. by apply/eqP => /Hcol; move: hh1t => /= /andP[-> _]. rewrite /= ltnS; move/IH: hh1t; by apply. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext