proposition: Lemma bipartite_cycle_even cy : colorable g kind -> path.cycle g cy -> ~~ odd (size cy).
proof: Proof. case: cy => //= h t Hcol Hcycle; apply/negP => abs. suff /Hcol : kind (last h t) = kind h. move: Hcycle; by rewrite rcons_path => /andP[_ ->]. apply/esym. rewrite -nth_last (_ : nth _ _ _ = nth h (h :: t) (size t)); last by destruct t. rewrite -(odd_double_half (size t)) (negbTE abs) add0n. apply (bipartite_path_kind_even Hcol) => //. move: Hcycle; by rewrite /= rcons_path => /andP[]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext