proposition: Lemma bipartite_path_kind_next : colorable g kind -> forall t h, path g h t -> forall i h0, i < (size t).-1 -> kind (nth h0 (h :: t) i) = kind (nth h0 (h :: t) i.+2).
proof: Proof. move=> Hcol [//|t1 [//|t2 t3]] h /= /and3P[ht1 t1t2 t2t3] i h0 it3. have H : path g h [:: t1, t2 & t3] by rewrite /= ht1 t1t2. move/(colorable_path_kind Hcol) : (H) => /= /(_ i.+1 h0). rewrite ltnS it3 => /(_ isT) /= H1; apply/eqP. move/(colorable_path_kind Hcol) : H => /= /(_ i h0). rewrite ltnS ltnW // => /(_ isT); move: (kind _) (kind _) (kind _) H1. by move=> -[] [|[|a]] ? -[] [|[|b]] ? // -[] [|[|c]] ?. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext