proposition: Lemma even_cycle_Knm n m (s : seq 'K_n,m) : cycle (--) s -> ~~ odd (size s).
proof: Proof. suff: bipartition [set x : 'K_n,m | x] by apply: bipartition_cycle. by move => [x|x] [y|y] //= _; rewrite !inE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)