proposition: Lemma bipartite_path_kind_even : colorable g kind -> forall i h0 t h, path g h t -> i <= (size t)./2 -> kind h = kind (nth h0 (h :: t) i.*2).
proof: Proof. move=> Hcol; elim=> // i IH h [//|t1 [//|t2 t3]] h0 ht it2. rewrite -[in RHS]muln2 mulSn add2n muln2 -(bipartite_path_kind_next Hcol) //. apply IH => //; by rewrite (leq_trans _ it2). move: it2 => /=. rewrite ltnS -(@leq_pmul2r 2) // !muln2 => /leq_ltn_trans; apply. by rewrite -{2}(odd_double_half (size t3)) ltnS leq_addl. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext