proposition: Lemma proper_separation_symmetry V1 V2 : proper_separation V1 V2 <-> proper_separation V2 V1.
proof: Proof. rewrite /proper_separation separation_sym. by firstorder. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)