proposition: Lemma cp_sym x y : cp x y = cp y x.
proof: Proof. Proof using. wlog suff S : x y / cp x y \subset cp y x. { apply/eqP. by rewrite eqEsubset !S. } apply/subsetP => z /cpP H. apply/cpP => p. move: (H (prev p)). by rewrite mem_prev. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)