proposition: Lemma separation_sym V1 V2 : separation V1 V2 <-> separation V2 V1.
proof: Proof. wlog suff W : V1 V2 / separation V1 V2 -> separation V2 V1. { split; exact: W. } move => sepV. split => [x|x1 x2 A B]; by rewrite 1?setUC 1?sgP sepV. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)