proposition: Lemma bipartition_cycle (G : diGraph) (A : {set G}) (s: seq G) : bipartition A -> cycle (--) s -> ~~ odd (size s).
proof: Proof. move => bipA; case: s => //= x s /(bipartition_path bipA); rewrite negbK. by rewrite last_rcons addbb size_rcons /= negbK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)