proposition: Lemma bipartition_path (G : diGraph) (A : {set G}) (x : G) (s: seq G) : bipartition A -> path (--) x s -> ~~ odd (((last x s \in A) (+) (x \in A)) + size s).
proof: Proof. move=> bipA; elim: s x => [|/= y s IH] x; first by rewrite addbb. move=> /andP[xy /IH]; rewrite (bipA _ _ xy) addbN. by case: (_ (+) _); rewrite //= negbK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)